[isabelle-dev] Float

[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.)

lemma "False" sorry is indeed a strange kind of markup... 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