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/Codegen/Thy/document/Foundations.tex
changeset 46563 0ad69b30b39c
parent 46523 7ca897381b26 
--- a/doc-src/Codegen/Thy/document/Foundations.tex	Tue Feb 21 12:45:00 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Foundations.tex	Tue Feb 21 13:10:13 2012 +0100
@@ -31,9 +31,9 @@
   components which can be customised individually.
 
   Conceptually all components operate on Isabelle's logic framework
-  \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}.  Practically, the object logic \hyperlink{theory.HOL}{\mbox{\isa{HOL}}}
+  \isa{Pure}.  Practically, the object logic \isa{HOL}
   provides the necessary facilities to make use of the code generator,
-  mainly since it is an extension of \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}.
+  mainly since it is an extension of \isa{Pure}.
 
   The constellation of the different components is visualized in the
   following picture.
isabelle