Am Montag, den 14.11.2011, 19:27 +0100 schrieb 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.
I want to enforce that the user needs to activate quick_and_dirty in ROOT.ML, to remind him that there is something 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. I added it to the ROOT.ML but not to Library.thy. So it is in the image file, but the user needs to explicitly load Coad_Real_Approx_By_Float to use it. I assume with this setup the Code generator setup is only available when the user explicitly imports Coad_Real_Approx_By_Float. > Cheers, > Florian - Johannes _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
