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