--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Sat Nov 10 14:31:18 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Sat Nov 10 14:31:20 2007 +0100
@@ -583,25 +583,25 @@
\begin{description}
- \item[\isa{Pretty{\isacharunderscore}Int}] represents \isa{HOL} integers by big
+ \item[\isa{Code{\isacharunderscore}Integer}] represents \isa{HOL} integers by big
integer literals in target languages.
- \item[\isa{Pretty{\isacharunderscore}Char}] represents \isa{HOL} characters by
+ \item[\isa{Code{\isacharunderscore}Char}] represents \isa{HOL} characters by
character literals in target languages.
- \item[\isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Pretty{\isacharunderscore}Char},
+ \item[\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Code{\isacharunderscore}Char},
but also offers treatment of character codes; includes
- \isa{Pretty{\isacharunderscore}Int}.
- \item[\isa{Executable{\isacharunderscore}Rat}] implements rational
- numbers.
- \item[\isa{Executable{\isacharunderscore}Real}] implements a subset of real numbers,
- namly those representable by rational numbers.
+ \isa{Code{\isacharunderscore}Integer}.
\item[\isa{Efficient{\isacharunderscore}Nat}] \label{eff_nat} implements natural numbers by integers,
which in general will result in higher efficency; pattern
matching with \isa{{\isadigit{0}}} / \isa{Suc}
- is eliminated; includes \isa{Pretty{\isacharunderscore}Int}.
- \item[\isa{ML{\isacharunderscore}String}] provides an additional datatype \isa{mlstring};
- in the \isa{HOL} default setup, strings in HOL are mapped to list
- of \isa{HOL} characters in SML; values of type \isa{mlstring} are
- mapped to strings in SML.
+ is eliminated; includes \isa{Code{\isacharunderscore}Integer}.
+ \item[\isa{Code{\isacharunderscore}Index}] 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.
+ \item[\isa{Code{\isacharunderscore}Message}] provides an additional datatype
+ \isa{message{\isacharunderscore}string} which is isomorphic to strings;
+ \isa{message{\isacharunderscore}string}s are mapped to target-language strings.
+ Useful for code setups which involve e.g. printing (error) messages.
\end{description}
@@ -1507,7 +1507,7 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexml{Code.add-func}\verb|Code.add_func: bool -> thm -> theory -> theory| \\
+ \indexml{Code.add-func}\verb|Code.add_func: thm -> theory -> theory| \\
\indexml{Code.del-func}\verb|Code.del_func: thm -> theory -> theory| \\
\indexml{Code.add-funcl}\verb|Code.add_funcl: string * thm list Susp.T -> theory -> theory| \\
\indexml{Code.add-inline}\verb|Code.add_inline: thm -> theory -> theory| \\
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/isabelle.sty Sat Nov 10 14:31:18 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/isabelle.sty Sat Nov 10 14:31:20 2007 +0100
@@ -20,15 +20,15 @@
%symbol markup -- \emph achieves decent spacing via italic corrections
\newcommand{\isamath}[1]{\emph{$#1$}}
\newcommand{\isatext}[1]{\emph{#1}}
-\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
+\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
-\newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
-\newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
-\newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
-\newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
+\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
+\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
+\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
+\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Sat Nov 10 14:31:18 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML Sat Nov 10 14:31:20 2007 +0100
@@ -9,7 +9,8 @@
structure List =
struct
-fun member A_ x (y :: ys) = HOL.eqop A_ x y orelse member A_ x ys
+fun member A_ x (y :: ys) =
+ (if HOL.eqop A_ y x then true else member A_ x ys)
| member A_ x [] = false;
end; (*struct List*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML Sat Nov 10 14:31:18 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML Sat Nov 10 14:31:20 2007 +0100
@@ -12,7 +12,8 @@
fun foldr f (x :: xs) a = f x (foldr f xs a)
| foldr f [] a = a;
-fun member A_ x (y :: ys) = HOL.eqop A_ x y orelse member A_ x ys
+fun member A_ x (y :: ys) =
+ (if HOL.eqop A_ y x then true else member A_ x ys)
| member A_ x [] = false;
end; (*struct List*)
@@ -26,10 +27,10 @@
fun insert x (Set xs) = Set (x :: xs);
-fun union xs (Set ys) = List.foldr insert ys xs;
+fun uniona xs (Set ys) = List.foldr insert ys xs;
fun member A_ x (Set xs) = List.member A_ x xs;
-fun uniona (Set xs) = List.foldr union xs empty;
+fun unionaa (Set xs) = List.foldr uniona xs empty;
end; (*struct Set*)
--- a/doc-src/TutorialI/Protocol/document/Message.tex Sat Nov 10 14:31:18 2007 +0100
+++ b/doc-src/TutorialI/Protocol/document/Message.tex Sat Nov 10 14:31:20 2007 +0100
@@ -50,7 +50,7 @@
\isacommand{types}\isamarkupfalse%
\ key\ {\isacharequal}\ nat\isanewline
\isacommand{consts}\isamarkupfalse%
-\ invKey\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}key{\isacharequal}{\isachargreater}key{\isachardoublequoteclose}%
+\ invKey\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}key\ {\isasymRightarrow}\ key{\isachardoublequoteclose}%
\isadelimproof
%
\endisadelimproof
--- a/doc-src/TutorialI/Protocol/document/Public.tex Sat Nov 10 14:31:18 2007 +0100
+++ b/doc-src/TutorialI/Protocol/document/Public.tex Sat Nov 10 14:31:20 2007 +0100
@@ -18,18 +18,16 @@
\begin{isamarkuptext}%
The function
\isa{pubK} maps agents to their public keys. The function
-\isa{priK} maps agents to their private keys. It is defined in terms of
-\isa{invKey} and \isa{pubK} by a translation; therefore \isa{priK} is
-not a proper constant, so we declare it using \isacommand{syntax}
-(cf.\ \S\ref{sec:syntax-translations}).%
+\isa{priK} maps agents to their private keys. It is merely
+an abbreviation (cf.\ \S\ref{sec:abbreviations}) defined in terms of
+\isa{invKey} and \isa{pubK}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\isamarkupfalse%
-\ pubK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isacharequal}{\isachargreater}\ key{\isachardoublequoteclose}\isanewline
-\isacommand{syntax}\isamarkupfalse%
-\ priK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isacharequal}{\isachargreater}\ key{\isachardoublequoteclose}\isanewline
-\isacommand{translations}\isamarkupfalse%
-\ {\isachardoublequoteopen}priK\ x{\isachardoublequoteclose}\ {\isasymrightleftharpoons}\ {\isachardoublequoteopen}invKey{\isacharparenleft}pubK\ x{\isacharparenright}{\isachardoublequoteclose}%
+\ pubK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isasymRightarrow}\ key{\isachardoublequoteclose}\isanewline
+\isacommand{abbreviation}\isamarkupfalse%
+\ priK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isasymRightarrow}\ key{\isachardoublequoteclose}\isanewline
+\isakeyword{where}\ {\isachardoublequoteopen}priK\ x\ \ {\isasymequiv}\ \ invKey{\isacharparenleft}pubK\ x{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
The set \isa{bad} consists of those agents whose private keys are known to
@@ -43,7 +41,7 @@
\isacommand{axioms}\isamarkupfalse%
\isanewline
\ \ inj{\isacharunderscore}pubK{\isacharcolon}\ \ \ \ \ \ \ \ {\isachardoublequoteopen}inj\ pubK{\isachardoublequoteclose}\isanewline
-\ \ priK{\isacharunderscore}neq{\isacharunderscore}pubK{\isacharcolon}\ \ \ {\isachardoublequoteopen}priK\ A\ {\isachartilde}{\isacharequal}\ pubK\ B{\isachardoublequoteclose}%
+\ \ priK{\isacharunderscore}neq{\isacharunderscore}pubK{\isacharcolon}\ \ \ {\isachardoublequoteopen}priK\ A\ {\isasymnoteq}\ pubK\ B{\isachardoublequoteclose}%
\isadelimproof
%
\endisadelimproof