*To*: Christian Sternagel <christian.sternagel at uibk.ac.at>*Subject*: Re: [isabelle] Isabelle Proof in Papers*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Thu, 21 Jan 2010 10:08:16 +0000*Cc*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <4B56E948.20808@uibk.ac.at>*References*: <4B56E948.20808@uibk.ac.at>

I prefer to keep my papers and my proofs quite separate. Sometimes I use Isabelle to generate laTeX material, which I process in various ways and insert into documents. This approach allows you to use integrated TeX environments and have full control over the appearance. Larry Paulson On 20 Jan 2010, at 11:30, Christian Sternagel wrote: > Hi there, > > currently I'm the first time using Isabelle/HOL for writing a paper. Thanks to Alexander Krauss, most of my initial questions were resolved. > > Initially I wrote my paper as an Isabelle theory Paper.thy, depending on my actual Isabelle/HOL developments. At first, I just stated my lemmas and filled the gaps with some "glue text" to explain everything. Additionally I set up a theory Setup.thy just for introducing notations I wanted to use in the paper. At this stage everything worked fine. > > However, I also wanted to give a textual sketch of every proof that was used for my lemmas. My Idea was to redo every proof that I wanted to describe inside Paper.thy. Then I wanted to hide all Isar commands (using (*<*) and (*>*)), replace them by "glue text" and refer to intermediate formulas, e.g., instead of > > have "A" by (auto simp: very powerful lemmas) > hence "B" by (auto simp: even more powerful lemmas) > > I would like to have > > ... we obtain A by using Lemmas x--y. From > this we conclude B using ... > > What I tried to do was > > txt {* ... we obtain *} > (*<*)have(*>*) "A" by %invisible (auto ...) > txt {* by using Lemmas x--y. From this we conclude *} > (*<*)hence(*>*) "B" by %invisible (auto ...) > txt {* using ... *} > > The result looks horrible :) and furthermore, no notations from Setup.thy are used. Hence my question: Is there a (preferably easy and nice) way to do what I want? What do others do in such situations? > > Maybe I should also give at least one reason, why I want to do what I showed above. Of course, I would like to rely on Isabelle to check all my displayed formulas in the background. Additionally, I do not want the reader (and especially the reviewer) to see any difference to a paper, just typeset with LaTeX without using Isabelle. My fear is, that reviewers wouldn't like to have to read Isabelle proofs (this surely depends on where you send your paper). > > cheers > > chris > >

**References**:**[isabelle] Isabelle Proof in Papers***From:*Christian Sternagel

- Previous by Date: [isabelle] Using Word, Map and Set in Haskabelle
- Next by Date: Re: [isabelle] Isabelle Proof in Papers
- Previous by Thread: [isabelle] Isabelle Proof in Papers
- Next by Thread: Re: [isabelle] Isabelle Proof in Papers
- Cl-isabelle-users January 2010 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