Re: [isabelle] Undefined facts in skip_proofs mode

On Wed, 30 Jul 2014, Cornelius Diekmann wrote:

So what did have have in mind when using it? It might explain the confusion.

I wanted to use skip_proofs to build the pdf proof documents _fast_ to
debug latex and formatting problems.

Which proof documents actually? When I have this situation, the time is usually spent on latex (several sequential runs), not the proofs (which run in parallel anyway).

In the longer run, the document preparation should become part of the Prover IDE -- but so far it did not worked out due to too many odd options and "modes" of the system in that particular respect.


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