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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
