Re: [isabelle] set quick_and_dirty mode when running Isabelle from the command line?
On Tue, 27 Sep 2011, Anh Le wrote:
I run Isabelle by the command "./isabelle usedir -b HOL Output" with the
input file name declared in ROOT.ML. How to set quick_and_dirty mode
from that command? I need to do that because I use some raw proof
Just include this in ROOT.ML:
quick_and_dirty := true;
What do you mean by "raw proof blocks" anyway?
This archive was generated by a fusion of
Pipermail (Mailman edition) and