updated;
authorwenzelm
Tue Oct 16 17:07:40 2007 +0200 (2007-10-16)
changeset 25056743f3603ba8b
parent 25055 3bb2ad8b1b37
child 25057 021fcbe2aaa5
updated;
doc-src/AxClass/Group/document/isabelle.sty
doc-src/IsarAdvanced/Classes/Thy/document/isabelle.sty
doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml
doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML
doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML
doc-src/IsarAdvanced/Functions/Thy/document/isabelle.sty
doc-src/IsarImplementation/Thy/document/isabelle.sty
doc-src/IsarOverview/Isar/document/Induction.tex
doc-src/IsarOverview/Isar/document/isabelle.sty
doc-src/LaTeXsugar/Sugar/document/isabelle.sty
doc-src/Locales/Locales/document/isabelle.sty
doc-src/TutorialI/Misc/document/AdvancedInd.tex
doc-src/TutorialI/Types/document/Numbers.tex
doc-src/TutorialI/Types/document/Records.tex
doc-src/TutorialI/isabelle.sty
doc-src/ZF/isabelle.sty
     1.1 --- a/doc-src/AxClass/Group/document/isabelle.sty	Tue Oct 16 17:06:21 2007 +0200
     1.2 +++ b/doc-src/AxClass/Group/document/isabelle.sty	Tue Oct 16 17:07:40 2007 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  %symbol markup -- \emph achieves decent spacing via italic corrections
     1.5  \newcommand{\isamath}[1]{\emph{$#1$}}
     1.6  \newcommand{\isatext}[1]{\emph{#1}}
     1.7 -\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
     1.8 +\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
     1.9  \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    1.10  \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    1.11  \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
     2.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/isabelle.sty	Tue Oct 16 17:06:21 2007 +0200
     2.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/isabelle.sty	Tue Oct 16 17:07:40 2007 +0200
     2.3 @@ -20,7 +20,7 @@
     2.4  %symbol markup -- \emph achieves decent spacing via italic corrections
     2.5  \newcommand{\isamath}[1]{\emph{$#1$}}
     2.6  \newcommand{\isatext}[1]{\emph{#1}}
     2.7 -\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
     2.8 +\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
     2.9  \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    2.10  \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    2.11  \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
     3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Tue Oct 16 17:06:21 2007 +0200
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Tue Oct 16 17:07:40 2007 +0200
     3.3 @@ -10,8 +10,11 @@
     3.4  heada (x : xs) = x;
     3.5  heada [] = Codegen.nulla;
     3.6  
     3.7 +null_option :: Maybe a;
     3.8 +null_option = Nothing;
     3.9 +
    3.10  instance Codegen.Null (Maybe a) where {
    3.11 -  nulla = Nothing;
    3.12 +  nulla = Codegen.null_option;
    3.13  };
    3.14  
    3.15  dummy :: Maybe Nat.Nat;
     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Tue Oct 16 17:06:21 2007 +0200
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Tue Oct 16 17:07:40 2007 +0200
     4.3 @@ -14,9 +14,11 @@
     4.4  fun head B_ (x :: xs) = x
     4.5    | head B_ [] = null B_;
     4.6  
     4.7 -fun null_option () = {null = NONE} : ('a option) null;
     4.8 +val null_option : 'a option = NONE;
     4.9 +
    4.10 +fun null_optiona () = {null = null_option} : ('a option) null;
    4.11  
    4.12  val dummy : Nat.nat option =
    4.13 -  head (null_option ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
    4.14 +  head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
    4.15  
    4.16  end; (*struct Codegen*)
     5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Tue Oct 16 17:06:21 2007 +0200
     5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Tue Oct 16 17:07:40 2007 +0200
     5.3 @@ -14,9 +14,11 @@
     5.4  let rec head _B = function x :: xs -> x
     5.5                    | [] -> null _B;;
     5.6  
     5.7 -let null_option () = ({null = None} : ('a option) null);;
     5.8 +let rec null_option = None;;
     5.9 +
    5.10 +let null_optiona () = ({null = null_option} : ('a option) null);;
    5.11  
    5.12  let rec dummy
    5.13 -  = head (null_option ()) [Some (Nat.Suc Nat.Zero_nat); None];;
    5.14 +  = head (null_optiona ()) [Some (Nat.Suc Nat.Zero_nat); None];;
    5.15  
    5.16  end;; (*struct Codegen*)
     6.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Tue Oct 16 17:06:21 2007 +0200
     6.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Tue Oct 16 17:07:40 2007 +0200
     6.3 @@ -11,9 +11,14 @@
     6.4  fun plus_nat (Suc m) n = plus_nat m (Suc n)
     6.5    | plus_nat Zero_nat n = n;
     6.6  
     6.7 -fun prod_case f1 (a, b) = f1 a b;
     6.8 +end; (*struct Nat*)
     6.9  
    6.10 -end; (*struct Nat*)
    6.11 +structure Product_Type = 
    6.12 +struct
    6.13 +
    6.14 +fun split c (a, b) = c a b;
    6.15 +
    6.16 +end; (*struct Product_Type*)
    6.17  
    6.18  structure List = 
    6.19  struct
     7.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Tue Oct 16 17:06:21 2007 +0200
     7.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Tue Oct 16 17:07:40 2007 +0200
     7.3 @@ -19,9 +19,14 @@
     7.4    | minus_nat Zero_nat n = Zero_nat
     7.5    | minus_nat m Zero_nat = m;
     7.6  
     7.7 -fun prod_case f1 (a, b) = f1 a b;
     7.8 +end; (*struct Nat*)
     7.9  
    7.10 -end; (*struct Nat*)
    7.11 +structure Product_Type = 
    7.12 +struct
    7.13 +
    7.14 +fun split c (a, b) = c a b;
    7.15 +
    7.16 +end; (*struct Product_Type*)
    7.17  
    7.18  structure Codegen = 
    7.19  struct
    7.20 @@ -30,7 +35,8 @@
    7.21    (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
    7.22    | pick (x :: xs) n =
    7.23      let
    7.24 -      val (k, v) = x;
    7.25 +      val a = x;
    7.26 +      val (k, v) = a;
    7.27      in
    7.28        (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
    7.29      end;
     8.1 --- a/doc-src/IsarAdvanced/Functions/Thy/document/isabelle.sty	Tue Oct 16 17:06:21 2007 +0200
     8.2 +++ b/doc-src/IsarAdvanced/Functions/Thy/document/isabelle.sty	Tue Oct 16 17:07:40 2007 +0200
     8.3 @@ -20,7 +20,7 @@
     8.4  %symbol markup -- \emph achieves decent spacing via italic corrections
     8.5  \newcommand{\isamath}[1]{\emph{$#1$}}
     8.6  \newcommand{\isatext}[1]{\emph{#1}}
     8.7 -\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
     8.8 +\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
     8.9  \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    8.10  \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    8.11  \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
     9.1 --- a/doc-src/IsarImplementation/Thy/document/isabelle.sty	Tue Oct 16 17:06:21 2007 +0200
     9.2 +++ b/doc-src/IsarImplementation/Thy/document/isabelle.sty	Tue Oct 16 17:07:40 2007 +0200
     9.3 @@ -20,7 +20,7 @@
     9.4  %symbol markup -- \emph achieves decent spacing via italic corrections
     9.5  \newcommand{\isamath}[1]{\emph{$#1$}}
     9.6  \newcommand{\isatext}[1]{\emph{#1}}
     9.7 -\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
     9.8 +\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
     9.9  \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    9.10  \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    9.11  \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    10.1 --- a/doc-src/IsarOverview/Isar/document/Induction.tex	Tue Oct 16 17:06:21 2007 +0200
    10.2 +++ b/doc-src/IsarOverview/Isar/document/Induction.tex	Tue Oct 16 17:07:40 2007 +0200
    10.3 @@ -431,13 +431,13 @@
    10.4  transitive closure of a relation --- HOL provides a predefined one as well.%
    10.5  \end{isamarkuptext}%
    10.6  \isamarkuptrue%
    10.7 -\isacommand{consts}\isamarkupfalse%
    10.8 -\ 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
    10.9 -\isacommand{inductive}\isamarkupfalse%
   10.10 -\ {\isachardoublequoteopen}r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
   10.11 -\isakeyword{intros}\isanewline
   10.12 -refl{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
   10.13 -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}%
   10.14 +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse%
   10.15 +\isanewline
   10.16 +\ \ 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
   10.17 +\ \ \isakeyword{for}\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\isanewline
   10.18 +\isakeyword{where}\isanewline
   10.19 +\ \ refl{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
   10.20 +{\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}%
   10.21  \begin{isamarkuptext}%
   10.22  \noindent
   10.23  First the constant is declared as a function on binary
    11.1 --- a/doc-src/IsarOverview/Isar/document/isabelle.sty	Tue Oct 16 17:06:21 2007 +0200
    11.2 +++ b/doc-src/IsarOverview/Isar/document/isabelle.sty	Tue Oct 16 17:07:40 2007 +0200
    11.3 @@ -20,7 +20,7 @@
    11.4  %symbol markup -- \emph achieves decent spacing via italic corrections
    11.5  \newcommand{\isamath}[1]{\emph{$#1$}}
    11.6  \newcommand{\isatext}[1]{\emph{#1}}
    11.7 -\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    11.8 +\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    11.9  \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
   11.10  \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
   11.11  \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    12.1 --- a/doc-src/LaTeXsugar/Sugar/document/isabelle.sty	Tue Oct 16 17:06:21 2007 +0200
    12.2 +++ b/doc-src/LaTeXsugar/Sugar/document/isabelle.sty	Tue Oct 16 17:07:40 2007 +0200
    12.3 @@ -20,7 +20,7 @@
    12.4  %symbol markup -- \emph achieves decent spacing via italic corrections
    12.5  \newcommand{\isamath}[1]{\emph{$#1$}}
    12.6  \newcommand{\isatext}[1]{\emph{#1}}
    12.7 -\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    12.8 +\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    12.9  \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
   12.10  \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
   12.11  \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    13.1 --- a/doc-src/Locales/Locales/document/isabelle.sty	Tue Oct 16 17:06:21 2007 +0200
    13.2 +++ b/doc-src/Locales/Locales/document/isabelle.sty	Tue Oct 16 17:07:40 2007 +0200
    13.3 @@ -20,7 +20,7 @@
    13.4  %symbol markup -- \emph achieves decent spacing via italic corrections
    13.5  \newcommand{\isamath}[1]{\emph{$#1$}}
    13.6  \newcommand{\isatext}[1]{\emph{#1}}
    13.7 -\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    13.8 +\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    13.9  \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
   13.10  \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
   13.11  \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    14.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Oct 16 17:06:21 2007 +0200
    14.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Oct 16 17:07:40 2007 +0200
    14.3 @@ -260,7 +260,7 @@
    14.4  \begin{isabelle}
    14.5  \isa{m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ Suc\ m\ {\isasymle}\ n}
    14.6  \rulename{Suc_leI}\isanewline
    14.7 -\isa{{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ j\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}
    14.8 +\isa{{\isasymlbrakk}x\ {\isasymle}\ y{\isacharsemicolon}\ y\ {\isacharless}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}\ z}
    14.9  \rulename{le_less_trans}
   14.10  \end{isabelle}
   14.11  %
    15.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Tue Oct 16 17:06:21 2007 +0200
    15.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Tue Oct 16 17:07:40 2007 +0200
    15.3 @@ -404,7 +404,7 @@
    15.4  FIELDS
    15.5  
    15.6  \begin{isabelle}%
    15.7 -a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachargreater}a{\isachardot}\ r\ {\isacharless}\ b%
    15.8 +x\ {\isacharless}\ y\ {\isasymLongrightarrow}\ {\isasymexists}z{\isachargreater}x{\isachardot}\ z\ {\isacharless}\ y%
    15.9  \end{isabelle}
   15.10  \rulename{dense}
   15.11  
    16.1 --- a/doc-src/TutorialI/Types/document/Records.tex	Tue Oct 16 17:06:21 2007 +0200
    16.2 +++ b/doc-src/TutorialI/Types/document/Records.tex	Tue Oct 16 17:07:40 2007 +0200
    16.3 @@ -547,22 +547,23 @@
    16.4    be the same as \isa{point{\isachardot}make}.
    16.5  
    16.6    \begin{isabelle}%
    16.7 -point{\isachardot}make\ Xcoord\ Ycoord\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isasymrparr}\isasep\isanewline%
    16.8 +point{\isachardot}make\ Xcoord\ Ycoord\ {\isasymequiv}\isanewline
    16.9 +{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}\isasep\isanewline%
   16.10  point{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline
   16.11  {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isasep\isanewline%
   16.12 -point{\isachardot}truncate\ r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}%
   16.13 +point{\isachardot}truncate\ r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}%
   16.14  \end{isabelle}
   16.15  
   16.16    Contrast those with the corresponding functions for record \isa{cpoint}.  Observe \isa{cpoint{\isachardot}fields} in particular.
   16.17  
   16.18    \begin{isabelle}%
   16.19  cpoint{\isachardot}make\ Xcoord\ Ycoord\ col\ {\isasymequiv}\isanewline
   16.20 -{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ col\ {\isacharequal}\ col{\isasymrparr}\isasep\isanewline%
   16.21 -cpoint{\isachardot}fields\ col\ {\isasymequiv}\ {\isasymlparr}col\ {\isacharequal}\ col{\isasymrparr}\isasep\isanewline%
   16.22 +{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ col\ {\isacharequal}\ col{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}\isasep\isanewline%
   16.23 +cpoint{\isachardot}fields\ col\ {\isasymequiv}\ {\isasymlparr}col\ {\isacharequal}\ col{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}\isasep\isanewline%
   16.24  cpoint{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline
   16.25  {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isasep\isanewline%
   16.26  cpoint{\isachardot}truncate\ r\ {\isasymequiv}\isanewline
   16.27 -{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isasymrparr}%
   16.28 +{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}%
   16.29  \end{isabelle}
   16.30  
   16.31    To demonstrate these functions, we declare a new coloured point by
    17.1 --- a/doc-src/TutorialI/isabelle.sty	Tue Oct 16 17:06:21 2007 +0200
    17.2 +++ b/doc-src/TutorialI/isabelle.sty	Tue Oct 16 17:07:40 2007 +0200
    17.3 @@ -20,7 +20,7 @@
    17.4  %symbol markup -- \emph achieves decent spacing via italic corrections
    17.5  \newcommand{\isamath}[1]{\emph{$#1$}}
    17.6  \newcommand{\isatext}[1]{\emph{#1}}
    17.7 -\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    17.8 +\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    17.9  \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
   17.10  \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
   17.11  \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    18.1 --- a/doc-src/ZF/isabelle.sty	Tue Oct 16 17:06:21 2007 +0200
    18.2 +++ b/doc-src/ZF/isabelle.sty	Tue Oct 16 17:07:40 2007 +0200
    18.3 @@ -20,7 +20,7 @@
    18.4  %symbol markup -- \emph achieves decent spacing via italic corrections
    18.5  \newcommand{\isamath}[1]{\emph{$#1$}}
    18.6  \newcommand{\isatext}[1]{\emph{#1}}
    18.7 -\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    18.8 +\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    18.9  \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
   18.10  \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
   18.11  \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}