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?


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