# HG changeset patch
# User wenzelm
# Date 1193140806 -7200
# Node ID 72fcf0832cfe7fbe6750a69897bf57966fa4e7a4
# Parent  1822da5446bc2e17779f226f5f6d29259818152b
updated;

diff -r 1822da5446bc -r 72fcf0832cfe doc-src/AxClass/Group/document/isabelle.sty
--- a/doc-src/AxClass/Group/document/isabelle.sty	Tue Oct 23 13:29:17 2007 +0200
+++ b/doc-src/AxClass/Group/document/isabelle.sty	Tue Oct 23 14:00:06 2007 +0200
@@ -25,10 +25,10 @@
 \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}}
diff -r 1822da5446bc -r 72fcf0832cfe doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Tue Oct 23 13:29:17 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Tue Oct 23 14:00:06 2007 +0200
@@ -3,6 +3,8 @@
 
 datatype nat = Suc of nat | Zero_nat;
 
+val one_nat : nat = Suc Zero_nat;
+
 fun plus_nat (Suc m) n = plus_nat m (Suc n)
   | plus_nat Zero_nat n = n;
 
@@ -15,6 +17,6 @@
 struct
 
 fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n)
-  | fac Nat.Zero_nat = Nat.Suc Nat.Zero_nat;
+  | fac Nat.Zero_nat = Nat.one_nat;
 
 end; (*struct Codegen*)
diff -r 1822da5446bc -r 72fcf0832cfe doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Tue Oct 23 13:29:17 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Tue Oct 23 14:00:06 2007 +0200
@@ -3,6 +3,8 @@
 
 datatype nat = Suc of nat | Zero_nat;
 
+val one_nat : nat = Suc Zero_nat;
+
 fun nat_case f1 f2 Zero_nat = f1
   | nat_case f1 f2 (Suc nat) = f2 nat;
 
@@ -18,7 +20,7 @@
 struct
 
 fun fac n =
-  (case n of Nat.Zero_nat => Nat.Suc Nat.Zero_nat
+  (case n of Nat.Zero_nat => Nat.one_nat
      | Nat.Suc m => Nat.times_nat n (fac m));
 
 end; (*struct Codegen*)
diff -r 1822da5446bc -r 72fcf0832cfe doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex
--- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Tue Oct 23 13:29:17 2007 +0200
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Tue Oct 23 14:00:06 2007 +0200
@@ -1303,7 +1303,7 @@
 \ findzero{\isachardot}domintros%
 \begin{isamarkuptext}%
 \begin{isabelle}%
-{\isacharparenleft}{\isadigit{0}}\ {\isacharless}\ {\isacharquery}f\ {\isacharquery}n\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}%
+{\isacharparenleft}{\isacharquery}f\ {\isacharquery}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ Suc\ {\isacharquery}n{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ findzero{\isacharunderscore}dom\ {\isacharparenleft}{\isacharquery}f{\isacharcomma}\ {\isacharquery}n{\isacharparenright}%
 \end{isabelle}
 
   Domain introduction rules allow to show that a given value lies in the
diff -r 1822da5446bc -r 72fcf0832cfe doc-src/IsarAdvanced/Functions/Thy/document/isabelle.sty
--- a/doc-src/IsarAdvanced/Functions/Thy/document/isabelle.sty	Tue Oct 23 13:29:17 2007 +0200
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/isabelle.sty	Tue Oct 23 14:00:06 2007 +0200
@@ -25,10 +25,10 @@
 \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}}
diff -r 1822da5446bc -r 72fcf0832cfe doc-src/IsarOverview/Isar/document/isabelle.sty
--- a/doc-src/IsarOverview/Isar/document/isabelle.sty	Tue Oct 23 13:29:17 2007 +0200
+++ b/doc-src/IsarOverview/Isar/document/isabelle.sty	Tue Oct 23 14:00:06 2007 +0200
@@ -25,10 +25,10 @@
 \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}}
diff -r 1822da5446bc -r 72fcf0832cfe doc-src/LaTeXsugar/Sugar/document/isabelle.sty
--- a/doc-src/LaTeXsugar/Sugar/document/isabelle.sty	Tue Oct 23 13:29:17 2007 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/isabelle.sty	Tue Oct 23 14:00:06 2007 +0200
@@ -25,10 +25,10 @@
 \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}}
diff -r 1822da5446bc -r 72fcf0832cfe doc-src/Locales/Locales/document/isabelle.sty
--- a/doc-src/Locales/Locales/document/isabelle.sty	Tue Oct 23 13:29:17 2007 +0200
+++ b/doc-src/Locales/Locales/document/isabelle.sty	Tue Oct 23 14:00:06 2007 +0200
@@ -25,10 +25,10 @@
 \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}}
diff -r 1822da5446bc -r 72fcf0832cfe doc-src/TutorialI/isabelle.sty
--- a/doc-src/TutorialI/isabelle.sty	Tue Oct 23 13:29:17 2007 +0200
+++ b/doc-src/TutorialI/isabelle.sty	Tue Oct 23 14:00:06 2007 +0200
@@ -25,10 +25,10 @@
 \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}}
diff -r 1822da5446bc -r 72fcf0832cfe doc-src/ZF/isabelle.sty
--- a/doc-src/ZF/isabelle.sty	Tue Oct 23 13:29:17 2007 +0200
+++ b/doc-src/ZF/isabelle.sty	Tue Oct 23 14:00:06 2007 +0200
@@ -25,10 +25,10 @@
 \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}}