Re: [isabelle] Build LaTex document without proof checking



On 2012/5/22 Makarius wrote:
> Toplevel.skip_proofs is still there as an add-on feature, and it should work
> in the same way as it ever did, what ever that means.

Thank you, that is exactly what I was looking for. An explanation how
to use this feature is already in the mailing list.

On Fri, 11 Feb 2011 16:16:11 Brian Huffman wrote:
>You can speed things up a bit by running Isabelle in "skip proofs"
>mode. Try adding commands to set the following two references before
>"use_thys" in ROOT.ML:
>
>quick_and_dirty := true;
>Toplevel.skip_proofs := true;
>use_thys ["MyTheory"];

Regards
  Cornelius





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