# HG changeset patch
# User wenzelm
# Date 1329826213 -3600
# Node ID 0ad69b30b39c1b491ac2957590e7b1422f132d00
# Parent  26977429b784d36da5d8745c47c10fd99082362f
updated generated files (cf. 8d51b375e926);

diff -r 26977429b784 -r 0ad69b30b39c doc-src/Codegen/Thy/document/Adaptation.tex
--- a/doc-src/Codegen/Thy/document/Adaptation.tex	Tue Feb 21 12:45:00 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex	Tue Feb 21 13:10:13 2012 +0100
@@ -149,7 +149,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{Main}}} theory already provides a code
+The \isa{HOL} \isa{Main} theory already provides a code
   generator setup which should be suitable for most applications.
   Common extensions and modifications are available by certain
   theories of the \isa{HOL} library; beside being useful in
@@ -173,12 +173,12 @@
        \isa{Suc} is eliminated; includes \isa{Code{\isaliteral{5F}{\isacharunderscore}}Integer}
        and \isa{Code{\isaliteral{5F}{\isacharunderscore}}Numeral}.
 
-    \item[\hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isaliteral{5F}{\isacharunderscore}}Numeral}}}] provides an additional datatype
+    \item[\isa{Code{\isaliteral{5F}{\isacharunderscore}}Numeral}] provides an additional datatype
        \isa{index} which is mapped to target-language built-in
        integers.  Useful for code setups which involve e.g.~indexing
        of target-language arrays.  Part of \isa{HOL{\isaliteral{2D}{\isacharminus}}Main}.
 
-    \item[\hyperlink{theory.String}{\mbox{\isa{String}}}] provides an additional datatype \isa{String{\isaliteral{2E}{\isachardot}}literal} which is isomorphic to strings; \isa{String{\isaliteral{2E}{\isachardot}}literal}s are mapped to target-language strings.  Useful
+    \item[\isa{String}] provides an additional datatype \isa{String{\isaliteral{2E}{\isachardot}}literal} which is isomorphic to strings; \isa{String{\isaliteral{2E}{\isachardot}}literal}s are mapped to target-language strings.  Useful
        for code setups which involve e.g.~printing (error) messages.
        Part of \isa{HOL{\isaliteral{2D}{\isacharminus}}Main}.
 
diff -r 26977429b784 -r 0ad69b30b39c doc-src/Codegen/Thy/document/Evaluation.tex
--- a/doc-src/Codegen/Thy/document/Evaluation.tex	Tue Feb 21 12:45:00 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex	Tue Feb 21 13:10:13 2012 +0100
@@ -372,7 +372,7 @@
   arbitrary ML code as well.
 
   A typical example for \hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}} can be found in the
-  \hyperlink{theory.Predicate}{\mbox{\isa{Predicate}}} theory.%
+  \isa{Predicate} theory.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 26977429b784 -r 0ad69b30b39c doc-src/Codegen/Thy/document/Foundations.tex
--- 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.
diff -r 26977429b784 -r 0ad69b30b39c doc-src/Codegen/Thy/document/Introduction.tex
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Tue Feb 21 12:45:00 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Tue Feb 21 13:10:13 2012 +0100
@@ -30,7 +30,7 @@
   \cite{scala-overview-tech-report}.
 
   To profit from this tutorial, some familiarity and experience with
-  \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \cite{isa-tutorial} and its basic theories is assumed.%
+  \isa{HOL} \cite{isa-tutorial} and its basic theories is assumed.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 26977429b784 -r 0ad69b30b39c doc-src/Codegen/Thy/document/Refinement.tex
--- a/doc-src/Codegen/Thy/document/Refinement.tex	Tue Feb 21 12:45:00 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Refinement.tex	Tue Feb 21 13:10:13 2012 +0100
@@ -628,9 +628,9 @@
 %
 \begin{isamarkuptext}%
 Typical data structures implemented by representations involving
-  invariants are available in the library, theory \hyperlink{theory.Mapping}{\mbox{\isa{Mapping}}}
+  invariants are available in the library, theory \isa{Mapping}
   specifies key-value-mappings (type \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ mapping});
-  these can be implemented by red-black-trees (theory \hyperlink{theory.RBT}{\mbox{\isa{RBT}}}).%
+  these can be implemented by red-black-trees (theory \isa{RBT}).%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %