# [isabelle] Isabelle Proof in Papers

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

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