[isabelle-dev] Float

[Florian Haftmann]

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.

Cheers,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>