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 blocks.

Just include this in ROOT.ML:

  quick_and_dirty := true;


What do you mean by "raw proof blocks" anyway?


	Makarius





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