# HG changeset patch
# User haftmann
# Date 1329592418 -3600
# Node ID 7ca897381b26ba38c541e4cb09a0c4f383d28d60
# Parent  2b1e87b3967f4c4c9e0f69cfce8fbbecc2c60e3d
update of generated documents

diff -r 2b1e87b3967f -r 7ca897381b26 doc-src/Codegen/Thy/document/Adaptation.tex
--- a/doc-src/Codegen/Thy/document/Adaptation.tex	Sat Feb 18 20:12:37 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex	Sat Feb 18 20:13:38 2012 +0100
@@ -158,33 +158,35 @@
 
   \begin{description}
 
-    \item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isaliteral{5F}{\isacharunderscore}}Integer}}}] represents \isa{HOL} integers by
+    \item[\isa{Code{\isaliteral{5F}{\isacharunderscore}}Integer}] represents \isa{HOL} integers by
        big integer literals in target languages.
 
-    \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isaliteral{5F}{\isacharunderscore}}Char}}}] represents \isa{HOL} characters by
+    \item[\isa{Code{\isaliteral{5F}{\isacharunderscore}}Char}] represents \isa{HOL} characters by
        character literals in target languages.
 
-    \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isaliteral{5F}{\isacharunderscore}}Char{\isaliteral{5F}{\isacharunderscore}}chr}}}] like \isa{Code{\isaliteral{5F}{\isacharunderscore}}Char}, but
-       also offers treatment of character codes; includes \hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isaliteral{5F}{\isacharunderscore}}Char}}}.
+    \item[\isa{Code{\isaliteral{5F}{\isacharunderscore}}Char{\isaliteral{5F}{\isacharunderscore}}chr}] like \isa{Code{\isaliteral{5F}{\isacharunderscore}}Char}, but
+       also offers treatment of character codes; includes \isa{Code{\isaliteral{5F}{\isacharunderscore}}Char}.
 
-    \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isaliteral{5F}{\isacharunderscore}}Nat}}}] \label{eff_nat} implements
+    \item[\isa{Efficient{\isaliteral{5F}{\isacharunderscore}}Nat}] \label{eff_nat} implements
        natural numbers by integers, which in general will result in
        higher efficiency; pattern matching with \isa{{\isadigit{0}}} /
-       \isa{Suc} is eliminated; includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isaliteral{5F}{\isacharunderscore}}Integer}}}
-       and \hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isaliteral{5F}{\isacharunderscore}}Numeral}}}.
+       \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
        \isa{index} which is mapped to target-language built-in
        integers.  Useful for code setups which involve e.g.~indexing
-       of target-language arrays.
+       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
        for code setups which involve e.g.~printing (error) messages.
+       Part of \isa{HOL{\isaliteral{2D}{\isacharminus}}Main}.
 
   \end{description}
 
   \begin{warn}
-    When importing any of these theories, they should form the last
+    When importing any of those theories which are not part of
+    \isa{HOL{\isaliteral{2D}{\isacharminus}}Main}, they should form the last
     items in an import list.  Since these theories adapt the code
     generator setup in a non-conservative fashion, strange effects may
     occur otherwise.
@@ -641,6 +643,7 @@
 %
 \endisadelimtheory
 \isanewline
+\isanewline
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
diff -r 2b1e87b3967f -r 7ca897381b26 doc-src/Codegen/Thy/document/Evaluation.tex
--- a/doc-src/Codegen/Thy/document/Evaluation.tex	Sat Feb 18 20:12:37 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex	Sat Feb 18 20:13:38 2012 +0100
@@ -427,6 +427,7 @@
 %
 \endisadelimtheory
 \isanewline
+\isanewline
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
diff -r 2b1e87b3967f -r 7ca897381b26 doc-src/Codegen/Thy/document/Foundations.tex
--- a/doc-src/Codegen/Thy/document/Foundations.tex	Sat Feb 18 20:12:37 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Foundations.tex	Sat Feb 18 20:13:38 2012 +0100
@@ -178,7 +178,7 @@
   interface, transforming a list of function theorems to another list
   of function theorems, provided that neither the heading constant nor
   its type change.  The \isa{{\isadigit{0}}} / \isa{Suc} pattern
-  elimination implemented in theory \hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isaliteral{5F}{\isacharunderscore}}Nat}}} (see
+  elimination implemented in theory \isa{Efficient{\isaliteral{5F}{\isacharunderscore}}Nat} (see
   \secref{eff_nat}) uses this interface.
 
   \noindent The current setup of the preprocessor may be inspected
diff -r 2b1e87b3967f -r 7ca897381b26 doc-src/Codegen/Thy/document/Further.tex
--- a/doc-src/Codegen/Thy/document/Further.tex	Sat Feb 18 20:12:37 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Further.tex	Sat Feb 18 20:13:38 2012 +0100
@@ -38,7 +38,7 @@
     \item \isa{Scala} sacrifices Hindely-Milner type inference for a
       much more rich type system with subtyping etc.  For this reason
       type arguments sometimes have to be given explicitly in square
-      brackets (mimicing System F syntax).
+      brackets (mimicking System F syntax).
 
     \item In contrast to \isa{Haskell} where most specialities of
       the type system are implemented using \emph{type classes},
@@ -616,6 +616,7 @@
 %
 \endisadelimtheory
 \isanewline
+\isanewline
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
diff -r 2b1e87b3967f -r 7ca897381b26 doc-src/Codegen/Thy/document/Inductive_Predicate.tex
--- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex	Sat Feb 18 20:12:37 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex	Sat Feb 18 20:13:38 2012 +0100
@@ -332,10 +332,9 @@
 %
 \begin{isamarkuptext}%
 \begin{isabelle}%
-lexord\ r\ {\isaliteral{3D}{\isacharequal}}\isanewline
-{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\isanewline
-\isaindent{\ }{\isaliteral{5C3C6578697374733E}{\isasymexists}}a\ v{\isaliteral{2E}{\isachardot}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ v\ {\isaliteral{5C3C6F723E}{\isasymor}}\isanewline
-\isaindent{\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}a\ v{\isaliteral{2E}{\isachardot}}\ }{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}u\ a\ b\ v\ w{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r\ {\isaliteral{5C3C616E643E}{\isasymand}}\ x\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ v\ {\isaliteral{5C3C616E643E}{\isasymand}}\ y\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{40}{\isacharat}}\ b\ {\isaliteral{23}{\isacharhash}}\ w{\isaliteral{29}{\isacharparenright}}{\isaliteral{7D}{\isacharbraceright}}%
+lexordp\ r\ {\isaliteral{3F}{\isacharquery}}xs\ {\isaliteral{3F}{\isacharquery}}ys\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\isanewline
+{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}a\ v{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}ys\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}xs\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ v\ {\isaliteral{5C3C6F723E}{\isasymor}}\isanewline
+\isaindent{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}a\ v{\isaliteral{2E}{\isachardot}}\ }{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}u\ a\ b\ v\ w{\isaliteral{2E}{\isachardot}}\ r\ a\ b\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}xs\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ v\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}ys\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{40}{\isacharat}}\ b\ {\isaliteral{23}{\isacharhash}}\ w{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
 \end{isabelle}%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -360,13 +359,13 @@
 \isatagquote
 \isacommand{lemma}\isamarkupfalse%
 \ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5F}{\isacharunderscore}}pred{\isaliteral{5F}{\isacharunderscore}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}append\ xs\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ v{\isaliteral{29}{\isacharparenright}}\ ys\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ lexord\ r\ {\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}append\ xs\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ v{\isaliteral{29}{\isacharparenright}}\ ys\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ lexordp\ r\ xs\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \isacommand{lemma}\isamarkupfalse%
 \ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5F}{\isacharunderscore}}pred{\isaliteral{5F}{\isacharunderscore}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}append\ u\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ v{\isaliteral{29}{\isacharparenright}}\ xs\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ append\ u\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{23}{\isacharhash}}\ w{\isaliteral{29}{\isacharparenright}}\ ys\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ r\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ lexord\ r\ {\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}append\ u\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ v{\isaliteral{29}{\isacharparenright}}\ xs\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ append\ u\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{23}{\isacharhash}}\ w{\isaliteral{29}{\isacharparenright}}\ ys\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ r\ a\ b\isanewline
+\ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ lexordp\ r\ xs\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \isacommand{code{\isaliteral{5F}{\isacharunderscore}}pred}\isamarkupfalse%
-\ lexord%
+\ lexordp%
 \endisatagquote
 {\isafoldquote}%
 %
@@ -492,6 +491,7 @@
 %
 \endisadelimtheory
 \isanewline
+\isanewline
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
diff -r 2b1e87b3967f -r 7ca897381b26 doc-src/Codegen/Thy/document/Introduction.tex
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Sat Feb 18 20:12:37 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Sat Feb 18 20:13:38 2012 +0100
@@ -578,6 +578,7 @@
 %
 \endisadelimtheory
 \isanewline
+\isanewline
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
diff -r 2b1e87b3967f -r 7ca897381b26 doc-src/Codegen/Thy/document/Refinement.tex
--- a/doc-src/Codegen/Thy/document/Refinement.tex	Sat Feb 18 20:12:37 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Refinement.tex	Sat Feb 18 20:13:38 2012 +0100
@@ -628,11 +628,9 @@
 %
 \begin{isamarkuptext}%
 Typical data structures implemented by representations involving
-  invariants are available in the library, e.g.~theories \hyperlink{theory.Cset}{\mbox{\isa{Cset}}} and \hyperlink{theory.Mapping}{\mbox{\isa{Mapping}}} specify sets (type \isa{{\isaliteral{27}{\isacharprime}}a\ Cset{\isaliteral{2E}{\isachardot}}set}) and
-  key-value-mappings (type \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ mapping}) respectively;
-  these can be implemented by distinct lists as presented here as
-  example (theory \hyperlink{theory.Dlist}{\mbox{\isa{Dlist}}}) and red-black-trees respectively
-  (theory \hyperlink{theory.RBT}{\mbox{\isa{RBT}}}).%
+  invariants are available in the library, theory \hyperlink{theory.Mapping}{\mbox{\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}}}).%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -650,6 +648,7 @@
 %
 \endisadelimtheory
 \isanewline
+\isanewline
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex