--- a/doc-src/AxClass/Group/document/isabelle.sty Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/AxClass/Group/document/isabelle.sty Tue Oct 16 17:07:40 2007 +0200
@@ -20,7 +20,7 @@
%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}$}}
--- a/doc-src/IsarAdvanced/Classes/Thy/document/isabelle.sty Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/isabelle.sty Tue Oct 16 17:07:40 2007 +0200
@@ -20,7 +20,7 @@
%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}$}}
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Tue Oct 16 17:07:40 2007 +0200
@@ -10,8 +10,11 @@
heada (x : xs) = x;
heada [] = Codegen.nulla;
+null_option :: Maybe a;
+null_option = Nothing;
+
instance Codegen.Null (Maybe a) where {
- nulla = Nothing;
+ nulla = Codegen.null_option;
};
dummy :: Maybe Nat.Nat;
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML Tue Oct 16 17:07:40 2007 +0200
@@ -14,9 +14,11 @@
fun head B_ (x :: xs) = x
| head B_ [] = null B_;
-fun null_option () = {null = NONE} : ('a option) null;
+val null_option : 'a option = NONE;
+
+fun null_optiona () = {null = null_option} : ('a option) null;
val dummy : Nat.nat option =
- head (null_option ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
+ head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
end; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml Tue Oct 16 17:07:40 2007 +0200
@@ -14,9 +14,11 @@
let rec head _B = function x :: xs -> x
| [] -> null _B;;
-let null_option () = ({null = None} : ('a option) null);;
+let rec null_option = None;;
+
+let null_optiona () = ({null = null_option} : ('a option) null);;
let rec dummy
- = head (null_option ()) [Some (Nat.Suc Nat.Zero_nat); None];;
+ = head (null_optiona ()) [Some (Nat.Suc Nat.Zero_nat); None];;
end;; (*struct Codegen*)
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Tue Oct 16 17:07:40 2007 +0200
@@ -11,9 +11,14 @@
fun plus_nat (Suc m) n = plus_nat m (Suc n)
| plus_nat Zero_nat n = n;
-fun prod_case f1 (a, b) = f1 a b;
+end; (*struct Nat*)
-end; (*struct Nat*)
+structure Product_Type =
+struct
+
+fun split c (a, b) = c a b;
+
+end; (*struct Product_Type*)
structure List =
struct
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML Tue Oct 16 17:07:40 2007 +0200
@@ -19,9 +19,14 @@
| minus_nat Zero_nat n = Zero_nat
| minus_nat m Zero_nat = m;
-fun prod_case f1 (a, b) = f1 a b;
+end; (*struct Nat*)
-end; (*struct Nat*)
+structure Product_Type =
+struct
+
+fun split c (a, b) = c a b;
+
+end; (*struct Product_Type*)
structure Codegen =
struct
@@ -30,7 +35,8 @@
(if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
| pick (x :: xs) n =
let
- val (k, v) = x;
+ val a = x;
+ val (k, v) = a;
in
(if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
end;
--- a/doc-src/IsarAdvanced/Functions/Thy/document/isabelle.sty Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/isabelle.sty Tue Oct 16 17:07:40 2007 +0200
@@ -20,7 +20,7 @@
%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}$}}
--- a/doc-src/IsarImplementation/Thy/document/isabelle.sty Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/document/isabelle.sty Tue Oct 16 17:07:40 2007 +0200
@@ -20,7 +20,7 @@
%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}$}}
--- a/doc-src/IsarOverview/Isar/document/Induction.tex Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/IsarOverview/Isar/document/Induction.tex Tue Oct 16 17:07:40 2007 +0200
@@ -431,13 +431,13 @@
transitive closure of a relation --- HOL provides a predefined one as well.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ rtc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharunderscore}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
-\isacommand{inductive}\isamarkupfalse%
-\ {\isachardoublequoteopen}r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
-\isakeyword{intros}\isanewline
-refl{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
-step{\isacharcolon}\ \ {\isachardoublequoteopen}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}%
+\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse%
+\isanewline
+\ \ rtc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharunderscore}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
+\ \ \isakeyword{for}\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\isanewline
+\isakeyword{where}\isanewline
+\ \ refl{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
+{\isacharbar}\ step{\isacharcolon}\ \ {\isachardoublequoteopen}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
First the constant is declared as a function on binary
--- a/doc-src/IsarOverview/Isar/document/isabelle.sty Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/IsarOverview/Isar/document/isabelle.sty Tue Oct 16 17:07:40 2007 +0200
@@ -20,7 +20,7 @@
%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}$}}
--- a/doc-src/LaTeXsugar/Sugar/document/isabelle.sty Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/isabelle.sty Tue Oct 16 17:07:40 2007 +0200
@@ -20,7 +20,7 @@
%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}$}}
--- a/doc-src/Locales/Locales/document/isabelle.sty Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/Locales/Locales/document/isabelle.sty Tue Oct 16 17:07:40 2007 +0200
@@ -20,7 +20,7 @@
%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}$}}
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Oct 16 17:07:40 2007 +0200
@@ -260,7 +260,7 @@
\begin{isabelle}
\isa{m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ Suc\ m\ {\isasymle}\ n}
\rulename{Suc_leI}\isanewline
-\isa{{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ j\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}
+\isa{{\isasymlbrakk}x\ {\isasymle}\ y{\isacharsemicolon}\ y\ {\isacharless}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}\ z}
\rulename{le_less_trans}
\end{isabelle}
%
--- a/doc-src/TutorialI/Types/document/Numbers.tex Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Tue Oct 16 17:07:40 2007 +0200
@@ -404,7 +404,7 @@
FIELDS
\begin{isabelle}%
-a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachargreater}a{\isachardot}\ r\ {\isacharless}\ b%
+x\ {\isacharless}\ y\ {\isasymLongrightarrow}\ {\isasymexists}z{\isachargreater}x{\isachardot}\ z\ {\isacharless}\ y%
\end{isabelle}
\rulename{dense}
--- a/doc-src/TutorialI/Types/document/Records.tex Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/TutorialI/Types/document/Records.tex Tue Oct 16 17:07:40 2007 +0200
@@ -547,22 +547,23 @@
be the same as \isa{point{\isachardot}make}.
\begin{isabelle}%
-point{\isachardot}make\ Xcoord\ Ycoord\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isasymrparr}\isasep\isanewline%
+point{\isachardot}make\ Xcoord\ Ycoord\ {\isasymequiv}\isanewline
+{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}\isasep\isanewline%
point{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline
{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isasep\isanewline%
-point{\isachardot}truncate\ r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}%
+point{\isachardot}truncate\ r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}%
\end{isabelle}
Contrast those with the corresponding functions for record \isa{cpoint}. Observe \isa{cpoint{\isachardot}fields} in particular.
\begin{isabelle}%
cpoint{\isachardot}make\ Xcoord\ Ycoord\ col\ {\isasymequiv}\isanewline
-{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ col\ {\isacharequal}\ col{\isasymrparr}\isasep\isanewline%
-cpoint{\isachardot}fields\ col\ {\isasymequiv}\ {\isasymlparr}col\ {\isacharequal}\ col{\isasymrparr}\isasep\isanewline%
+{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ col\ {\isacharequal}\ col{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}\isasep\isanewline%
+cpoint{\isachardot}fields\ col\ {\isasymequiv}\ {\isasymlparr}col\ {\isacharequal}\ col{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}\isasep\isanewline%
cpoint{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline
{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isasep\isanewline%
cpoint{\isachardot}truncate\ r\ {\isasymequiv}\isanewline
-{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isasymrparr}%
+{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}%
\end{isabelle}
To demonstrate these functions, we declare a new coloured point by
--- a/doc-src/TutorialI/isabelle.sty Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/TutorialI/isabelle.sty Tue Oct 16 17:07:40 2007 +0200
@@ -20,7 +20,7 @@
%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}$}}
--- a/doc-src/ZF/isabelle.sty Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/ZF/isabelle.sty Tue Oct 16 17:07:40 2007 +0200
@@ -20,7 +20,7 @@
%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}$}}