| changeset 1846 | 763f08fb194f |
| parent 1590 | 1547174673e1 |
| child 1876 | b163e192a2bf |
--- a/doc-src/Ref/thm.tex Fri Jul 05 14:22:59 1996 +0200 +++ b/doc-src/Ref/thm.tex Thu Jul 11 15:00:38 1996 +0200 @@ -652,7 +652,7 @@ \index{meta-rules|)} -\section{Proof objects} +\section{Proof objects}\label{sec:proofObjects} \index{proof objects|(} Isabelle can record the full meta-level proof of each theorem. The proof object contains all logical inferences in detail, while omitting bookkeeping steps that have no logical meaning to an outside