--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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