[isabelle] skip_proofs in Isabelle2012



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"


I'm only seeing the error when I refer to paths explicitly in the import section and Isabelle actually resolves that path. That is, if I manually (in skip_proof mode) step through List_Prefix first and the theory is loaded, the import works fine. (That defeats the purpose of skip_proof mode, of course, because I'm trying to avoid stepping through 30 files and waiting for an hour).

Any ideas?

Cheers,
Gerwin






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