*To*: Gergely Buday <buday.gergely at uni-eszterhazy.hu>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] using oops in document preparation*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 12 Jul 2016 12:46:41 +0200*In-reply-to*: <005101d1dc0f$1645fa40$42d1eec0$@uni-eszterhazy.hu>*References*: <005101d1dc0f$1645fa40$42d1eec0$@uni-eszterhazy.hu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0

Hi Gergely,

lemma "~ False" proof (simp only: )(*<*)?(*>*) (*<*) oops (*>*) should do the job. Hope this helps, Andreas On 12/07/16 09:29, Gergely Buday wrote:

Hi, I have lemma "¬ False" proof (simp only: ) (*<*) oops (*>*) which leads to the Failed to apply initial proof method error message in the interactive development. oops recovers from the error and I can write other theorem statements. The Isabelle/Isar reference manual writes: A typical application of oops is to explain Isar proofs within the system itself, in conjunction with the document preparation tools of Isabelle described in chapter 4. Thus partial or even wrong proof attempts can be discussed in a logically sound manner. Note that the Isabelle LaTeX macros can be easily adapted to print something like "..." instead of the keyword "oops". When I use isabelle build -D . I get the same error as above and no output is produced. I tried -o quick_and_dirty but in vain. How can I include failed proof attempts into a proof document? I use Isabelle2016. - Gergely

**References**:**[isabelle] using oops in document preparation***From:*Gergely Buday

- Previous by Date: Re: [isabelle] using oops in document preparation
- Next by Date: Re: [isabelle] Some corrections and amendments
- Previous by Thread: Re: [isabelle] using oops in document preparation
- Next by Thread: [isabelle] using a remote server behind Isabelle/jEdit
- Cl-isabelle-users July 2016 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