Email Gateway (Aug 18 2022 at 18:26): Email Gateway (Aug 18 2022 at 18:26):From: Anh Le <anhlevn@cims.nyu.edu>
Hi everyone,
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.
Thank you very much
Anh
Email Gateway (Aug 18 2022 at 18:27):From: Makarius <makarius@sketis.net>
Just include this in ROOT.ML:
quick_and_dirty := true;
What do you mean by "raw proof blocks" anyway?
Makarius
Last updated: Apr 26 2024 at 04:17 UTC