Hey everyone,Maximilian (in cc) ported HOL-Light's decision procedure for metric spaces [1], and currently has two prototype implementations, one in Isabelle/ML, and the other one as an Eisbach method.
Now we are wondering which one to finalize and include in HOL-Analysis (the idea is to use it to automate and simplify proofs about metric spaces in the library, as well).
The Eisbach method is more readable and therefore easier to understand and maintain, but it would pull in Eisbach as an additional dependency.
Any opinions on whether or not adding Eisbach to the dependencies of HOL-Analysis would be a bad idea?
I remember that at some point, importing Eisbach changed the implementation of the "of" attribute or something like that and therefore caused some problems down the line.
(This is probably not relevant for Isabelle2019) Best regards, Fabian [1] https://arxiv.org/pdf/0904.3482
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
