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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
