Re: [isabelle] Different behavior in Jedit and Emacs



On Sat, Jan 21, 2012 at 12:48 AM, Peter Gammie <peteg42 at gmail.com> wrote:
> "sorry" only works if quick and dirty is switched on. I use that a lot when developing a proof interactively, as I expect everyone does.

Actually, you can use "sorry" in ProofGeneral even with
quick-and-dirty mode switched off, if you manually step through the
file(s) containing "sorry".

You only get the "Cheating requires quick_and_dirty mode!" error if an
import statement causes Isabelle to load a theory file containing
"sorry". The workaround is to pre-load any offending files
individually.

Of course, if you have a large collection of interconnected theories,
and you use "sorry" in many different files, this might be a pain. But
in that case, you are always free to turn quick-and-dirty mode back
on, at your own risk!

- Brian





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