Re: [isabelle] skip_proofs in Isabelle2012

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/ 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

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;"

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.

In the longer run, quick_and_dirty, 'sorry', skip_proofs and forked proofs should be all unified to forked proofs.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.