# HG changeset patch
# User wenzelm
# Date 1176384929 -7200
# Node ID 6cf96b9f7b9e7f6b2afebd3aca5630fc19a900ab
# Parent  8c6b4f7548e3cecb8e02c7707410c716f0671ebb
updated;

diff -r 8c6b4f7548e3 -r 6cf96b9f7b9e doc-src/AxClass/Group/document/isabelle.sty
--- a/doc-src/AxClass/Group/document/isabelle.sty	Thu Apr 12 15:01:13 2007 +0200
+++ b/doc-src/AxClass/Group/document/isabelle.sty	Thu Apr 12 15:35:29 2007 +0200
@@ -31,6 +31,7 @@
 \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
+\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 
 
 \newdimen\isa@parindent\newdimen\isa@parskip
diff -r 8c6b4f7548e3 -r 6cf96b9f7b9e doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Thu Apr 12 15:01:13 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Thu Apr 12 15:35:29 2007 +0200
@@ -559,7 +559,7 @@
 \ idem\ {\isacharless}\ type\isanewline
 \ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
-together with a corresponding interpretation:%
+\noindent together with a corresponding interpretation:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{interpretation}\isamarkupfalse%
diff -r 8c6b4f7548e3 -r 6cf96b9f7b9e doc-src/IsarAdvanced/Classes/Thy/document/isabelle.sty
--- a/doc-src/IsarAdvanced/Classes/Thy/document/isabelle.sty	Thu Apr 12 15:01:13 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/isabelle.sty	Thu Apr 12 15:35:29 2007 +0200
@@ -31,6 +31,7 @@
 \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
+\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 
 
 \newdimen\isa@parindent\newdimen\isa@parskip
diff -r 8c6b4f7548e3 -r 6cf96b9f7b9e doc-src/IsarImplementation/Thy/document/isabelle.sty
--- a/doc-src/IsarImplementation/Thy/document/isabelle.sty	Thu Apr 12 15:01:13 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/document/isabelle.sty	Thu Apr 12 15:35:29 2007 +0200
@@ -31,6 +31,7 @@
 \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
+\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 
 
 \newdimen\isa@parindent\newdimen\isa@parskip
diff -r 8c6b4f7548e3 -r 6cf96b9f7b9e doc-src/IsarOverview/Isar/document/isabelle.sty
--- a/doc-src/IsarOverview/Isar/document/isabelle.sty	Thu Apr 12 15:01:13 2007 +0200
+++ b/doc-src/IsarOverview/Isar/document/isabelle.sty	Thu Apr 12 15:35:29 2007 +0200
@@ -31,6 +31,7 @@
 \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
+\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 
 
 \newdimen\isa@parindent\newdimen\isa@parskip
diff -r 8c6b4f7548e3 -r 6cf96b9f7b9e doc-src/LaTeXsugar/Sugar/document/isabelle.sty
--- a/doc-src/LaTeXsugar/Sugar/document/isabelle.sty	Thu Apr 12 15:01:13 2007 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/isabelle.sty	Thu Apr 12 15:35:29 2007 +0200
@@ -31,6 +31,7 @@
 \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
+\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 
 
 \newdimen\isa@parindent\newdimen\isa@parskip
diff -r 8c6b4f7548e3 -r 6cf96b9f7b9e doc-src/Locales/Locales/document/isabelle.sty
--- a/doc-src/Locales/Locales/document/isabelle.sty	Thu Apr 12 15:01:13 2007 +0200
+++ b/doc-src/Locales/Locales/document/isabelle.sty	Thu Apr 12 15:35:29 2007 +0200
@@ -31,6 +31,7 @@
 \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
+\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 
 
 \newdimen\isa@parindent\newdimen\isa@parskip
diff -r 8c6b4f7548e3 -r 6cf96b9f7b9e doc-src/TutorialI/Misc/document/appendix.tex
--- a/doc-src/TutorialI/Misc/document/appendix.tex	Thu Apr 12 15:01:13 2007 +0200
+++ b/doc-src/TutorialI/Misc/document/appendix.tex	Thu Apr 12 15:35:29 2007 +0200
@@ -35,8 +35,8 @@
 \isa{abs} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & ${\mid} x {\mid}$\\
 \isa{{\isasymle}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
 \isa{{\isacharless}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
-\isa{min} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
-\isa{max} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
+\isa{Orderings{\isachardot}min} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
+\isa{Orderings{\isachardot}max} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
 \isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} &
 \isa{LEAST}$~x.~P$
 \end{tabular}
diff -r 8c6b4f7548e3 -r 6cf96b9f7b9e doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Thu Apr 12 15:01:13 2007 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Thu Apr 12 15:35:29 2007 +0200
@@ -154,7 +154,7 @@
 \isa{{\isasymand}}, \isa{{\isasymor}}, \isa{{\isasymlongrightarrow}}, \isa{{\isacharequal}},
 \isa{{\isasymforall}}, \isa{{\isasymexists}}), the relations \isa{{\isacharequal}},
 \isa{{\isasymle}} and \isa{{\isacharless}}, and the operations \isa{{\isacharplus}}, \isa{{\isacharminus}},
-\isa{min} and \isa{max}.  For example,%
+\isa{Orderings{\isachardot}min} and \isa{Orderings{\isachardot}max}.  For example,%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\isamarkupfalse%
diff -r 8c6b4f7548e3 -r 6cf96b9f7b9e doc-src/TutorialI/Types/document/Numbers.tex
--- a/doc-src/TutorialI/Types/document/Numbers.tex	Thu Apr 12 15:01:13 2007 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex	Thu Apr 12 15:35:29 2007 +0200
@@ -27,7 +27,7 @@
 \isacommand{ML}\isamarkupfalse%
 \ {\isachardoublequoteopen}Pretty{\isachardot}setmargin\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline
 \isacommand{ML}\isamarkupfalse%
-\ {\isachardoublequoteopen}IsarOutput{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
+\ {\isachardoublequoteopen}ThyOutput{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
 \endisatagML
 {\isafoldML}%
 %
diff -r 8c6b4f7548e3 -r 6cf96b9f7b9e doc-src/TutorialI/isabelle.sty
--- a/doc-src/TutorialI/isabelle.sty	Thu Apr 12 15:01:13 2007 +0200
+++ b/doc-src/TutorialI/isabelle.sty	Thu Apr 12 15:35:29 2007 +0200
@@ -31,6 +31,7 @@
 \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
+\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 
 
 \newdimen\isa@parindent\newdimen\isa@parskip
diff -r 8c6b4f7548e3 -r 6cf96b9f7b9e doc-src/ZF/isabelle.sty
--- a/doc-src/ZF/isabelle.sty	Thu Apr 12 15:01:13 2007 +0200
+++ b/doc-src/ZF/isabelle.sty	Thu Apr 12 15:35:29 2007 +0200
@@ -31,6 +31,7 @@
 \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
+\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 
 
 \newdimen\isa@parindent\newdimen\isa@parskip