[isabelle-dev] Float

[Johannes Hölzl]

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