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