Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/IsarImplementation/Thy/document/Proof.tex
changeset 46525 af3df09590f9
parent 46265 b6ab3cdea163 
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex	Sat Feb 18 20:50:11 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex	Sat Feb 18 20:53:39 2012 +0100
@@ -485,7 +485,7 @@
 \begin{isamarkuptext}%
 The following example demonstrates how rules can be
   derived by building up a context of assumptions first, and exporting
-  some local fact afterwards.  We refer to \hyperlink{theory.Pure}{\mbox{\isa{Pure}}} equality
+  some local fact afterwards.  We refer to \isa{Pure} equality
   here for testing purposes.%
 \end{isamarkuptext}%
 \isamarkuptrue%
isabelle