--- 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
--- 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%
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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}
--- 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%
--- 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}%
%
--- 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
--- 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