[isabelle-dev] Float

[Johannes Hölzl]

Am Montag, den 14.11.2011, 21:05 +0100 schrieb Alexander Krauss:
> On 11/14/2011 08:43 PM, Johannes Hölzl wrote:
> > 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.
> 
> This is rather non-standard and also breaks the test, cf.
> 
> http://isabelle.in.tum.de/reports/Isabelle/report/d6e6227d86634c02890a3e60e508abc3
> 
> (Tests are run without quick_and_dirty, and rightfully so.)

Oh, I didn't look at that. I removed the check now.

> lemma "False" sorry is indeed a strange kind of markup...

Well False is proven anyway, and it is a easy check for quick_and_dirty.

 - Johannes

> I remember 
> that the code generator has a notion of different "targets" (e.g., SML, 
> Haskell, Eval,...). @Florian: Is it imaginable to add such unsound setup 
> in a way that it does not infect the evaluation oracle by default?
> 
> Alex
> 
>