# HG changeset patch
# User wenzelm
# Date 1192547260 -7200
# Node ID 743f3603ba8bca00dc4c248947d1069854163e7b
# Parent  3bb2ad8b1b375d96409a9c57345e65a1463933dd
updated;

diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/AxClass/Group/document/isabelle.sty
--- 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}$}}
diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/IsarAdvanced/Classes/Thy/document/isabelle.sty
--- 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}$}}
diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
--- 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;
diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
--- 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*)
diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml
--- 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*)
diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML
--- 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
diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML
--- 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;
diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/IsarAdvanced/Functions/Thy/document/isabelle.sty
--- 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}$}}
diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/IsarImplementation/Thy/document/isabelle.sty
--- 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}$}}
diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/IsarOverview/Isar/document/Induction.tex
--- 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
diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/IsarOverview/Isar/document/isabelle.sty
--- 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}$}}
diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/LaTeXsugar/Sugar/document/isabelle.sty
--- 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}$}}
diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/Locales/Locales/document/isabelle.sty
--- 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}$}}
diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- 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}
 %
diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/TutorialI/Types/document/Numbers.tex
--- 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}
 
diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/TutorialI/Types/document/Records.tex
--- 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
diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/TutorialI/isabelle.sty
--- 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}$}}
diff -r 3bb2ad8b1b37 -r 743f3603ba8b doc-src/ZF/isabelle.sty
--- 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}$}}