# [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.