*To*: isabelle-users Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] skip_proofs in Isabelle2012*From*: Gerwin Klein <gerwin.klein at nicta.com.au>*Date*: Fri, 27 Jul 2012 09:17:01 +1000*In-reply-to*: <alpine.LNX.2.00.1207262031050.23425@macbroy21.informatik.tu-muenchen.de>*References*: <1DBCF519-87DF-446A-B899-F0D806CAEE26@nicta.com.au> <alpine.LNX.2.00.1207262031050.23425@macbroy21.informatik.tu-muenchen.de>

On 27/07/2012, at 4:34 AM, Makarius <makarius at sketis.net> wrote: > On Thu, 26 Jul 2012, Gerwin Klein wrote: > >> The skip_proofs option seems to clash with something in Isabelle2012. I'm getting "Messed-up outer syntax for presentation". >> >> Initially I thought this may be a PG problem, but it's not. I tried the following on the tty level: >> >> >> serenity:~ kleing$ /Applications/Isabelle2012.app/Isabelle/bin/isabelle tty >>> val it = (): unit >> val commit = fn: unit -> bool >> Welcome to Isabelle/HOL (Isabelle2012: May 2012) >>> theory X imports Main begin >> theory X >>> ML "quick_and_dirty := true"; >> val it = (): unit >> >>> ML "Toplevel.skip_proofs := true"; >> val it = (): unit >> >>> end; >>> theory A imports "~~/src/HOL/Library/List_Prefix" begin >> Loading theory "List_Prefix" >> *** Messed-up outer syntax for presentation >> *** At command "theory" > > The above should work if you include this as well: > > ML "Goal.parallel_proofs := 0;" Thanks, I can confirm that this works on our side. > I can't say on the spot what is the reason for this behaviour. A bit too many features have accumulated in the system, and everytime I pass by that part of the Isar toplevel, I wonder which combinations of the various flags actually work. I had a brief look at that code before I wrote the message and gave up, yes :-) > In the longer run, quick_and_dirty, 'sorry', skip_proofs and forked proofs should be all unified to forked proofs. That sounds reasonable. Cheers, Gerwin

**References**:**[isabelle] skip_proofs in Isabelle2012***From:*Gerwin Klein

**Re: [isabelle] skip_proofs in Isabelle2012***From:*Makarius

- Previous by Date: Re: [isabelle] Sledgehammer and Nitpick from the command line?
- Next by Date: Re: [isabelle] Sledgehammer and Nitpick from the command line?
- Previous by Thread: Re: [isabelle] skip_proofs in Isabelle2012
- Next by Thread: [isabelle] Sledgehammer and Nitpick from the command line?
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list