[isabelle-dev] Eisbach and HOL-Analysis

[Fabian Immler]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190430/fd53e615/attachment.bin>