hoelzl at in.tum.de
Mon Nov 14 20:43:52 CET 2011
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.
More information about the isabelle-dev