*To*: Gerwin Klein <gerwin.klein at nicta.com.au>*Subject*: Re: [isabelle] skip_proofs in Isabelle2012*From*: Makarius <makarius at sketis.net>*Date*: Thu, 26 Jul 2012 20:34:48 +0200 (CEST)*Cc*: isabelle-users Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <1DBCF519-87DF-446A-B899-F0D806CAEE26@nicta.com.au>*References*: <1DBCF519-87DF-446A-B899-F0D806CAEE26@nicta.com.au>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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 ttyval it = (): unitval commit = fn: unit -> bool Welcome to Isabelle/HOL (Isabelle2012: May 2012)theory X imports Main begintheory XML "quick_and_dirty := true";val it = (): unitML "Toplevel.skip_proofs := true";val it = (): unitend; theory A imports "~~/src/HOL/Library/List_Prefix" beginLoading 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;"

Makarius

**Follow-Ups**:**Re: [isabelle] skip_proofs in Isabelle2012***From:*Gerwin Klein

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

- Previous by Date: Re: [isabelle] HOLCF equality type class
- Next by Date: [isabelle] Proving a simple lemma
- Previous by Thread: [isabelle] skip_proofs in Isabelle2012
- Next by Thread: Re: [isabelle] skip_proofs in Isabelle2012
- 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