[isabelle-dev] Eisbach and HOL-Analysis
immler at in.tum.de
Tue Apr 30 17:33:14 CEST 2019
Maximilian (in cc) ported HOL-Light's decision procedure for metric
spaces , 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)
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev