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/TutorialI/Types/document/Axioms.tex
changeset 46525 af3df09590f9
parent 40406 313a24b66a8d 
--- a/doc-src/TutorialI/Types/document/Axioms.tex	Sat Feb 18 20:50:11 2012 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex	Sat Feb 18 20:53:39 2012 +0100
@@ -463,7 +463,7 @@
 \emph{with} axioms.
 
 Further note that classes may contain axioms but \emph{no} operations.
-An example is class \isa{finite} from theory \hyperlink{theory.Finite-Set}{\mbox{\isa{Finite{\isaliteral{5F}{\isacharunderscore}}Set}}}
+An example is class \isa{finite} from theory \isa{Finite{\isaliteral{5F}{\isacharunderscore}}Set}
 which specifies a type to be finite: \isa{{\isaliteral{22}{\isachardoublequote}}finite\ {\isaliteral{28}{\isacharparenleft}}UNIV\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}finite\ set{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
isabelle