*To*: Cornelius Diekmann <c.diekmann at googlemail.com>*Subject*: Re: [isabelle] Undefined facts in skip_proofs mode*From*: Makarius <makarius at sketis.net>*Date*: Wed, 30 Jul 2014 21:23:19 +0200 (CEST)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Lars Hupel <hupel at in.tum.de>*In-reply-to*: <CAGbqCMyOMt693hTHUSHmgCYqF7vLM2M=DSiv-Zs4N_2LZgz22g@mail.gmail.com>*References*: <53D64E5A.60405@in.tum.de> <alpine.LNX.2.00.1407292003190.58841@lxbroy10.informatik.tu-muenchen.de> <CAGbqCMyOMt693hTHUSHmgCYqF7vLM2M=DSiv-Zs4N_2LZgz22g@mail.gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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.

Makarius

**References**:**[isabelle] Undefined facts in skip_proofs mode***From:*Lars Hupel

**Re: [isabelle] Undefined facts in skip_proofs mode***From:*Makarius

- Previous by Date: [isabelle] @{make_string} and the ML_print_depth attribute
- Next by Date: Re: [isabelle] Defining Shortcut for Output-Panel: Update
- Previous by Thread: Re: [isabelle] Undefined facts in skip_proofs mode
- Next by Thread: Re: [isabelle] Undefined facts in skip_proofs mode
- Cl-isabelle-users July 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list