[isabelle-dev] Float

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Mon Nov 14 19:27:15 CET 2011

Hi Johannes,

two remarks:

* http://isabelle.in.tum.de/reports/Isabelle/rev/e828ccc5c110

With `notepad` you can prove everything without a trace in theory, which
eliminates the need for fiddling around with quick_and_dirty.

* http://isabelle.in.tum.de/reports/Isabelle/rev/34d07cf7d207

I would prefer to see nothing which violates the integrity of code
generation in the standard HOL-Library import.  You can add it to the
HOL-Library session, but not the Library theory, similarly to various
theories conflictingly instantiating type classes.  A separate test can
be added to HOL-ex then.




PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20111114/2018024b/attachment.asc>

More information about the isabelle-dev mailing list