[isabelle-dev] Float

Alexander Krauss krauss at in.tum.de
Mon Nov 14 21:05:17 CET 2011

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.


(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?


More information about the isabelle-dev mailing list