updated;

--- a/doc-src/AxClass/generated/isabelle.sty	Fri Aug 19 22:25:21 2005 +0200
+++ b/doc-src/AxClass/generated/isabelle.sty	Fri Aug 19 22:28:23 2005 +0200
@@ -3,6 +3,7 @@
 %%
 %% macros for Isabelle generated LaTeX output
 %%
+%% $Id$
 
 %%% Simple document preparation (based on theory token language and symbols)
 
@@ -21,10 +22,17 @@
 \newcommand{\isamath}[1]{\emph{$#1$}}
 \newcommand{\isatext}[1]{\emph{#1}}
 \newcommand{\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{\isactrlsub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
+\newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
+\newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
+\newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#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}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 
+
 \newdimen\isa@parindent\newdimen\isa@parskip
 
 \newenvironment{isabellebody}{%
@@ -40,7 +48,8 @@
 \newcommand{\isa}[1]{\emph{\isastyleminor #1}}
 
 \newcommand{\isaindent}[1]{\hphantom{#1}}
-\newcommand{\isanewline}{\mbox{}\\\mbox{}}
+\newcommand{\isanewline}{\mbox{}\par\mbox{}}
+\newcommand{\isasep}{} % override with e.g. \renewcommand{\isasep}{\vspace{1ex}}
 \newcommand{\isadigit}[1]{#1}
 
 \chardef\isacharbang=`\!
@@ -140,6 +149,7 @@
 \renewcommand{\isachargreater}{\isamath{>}}%
 \renewcommand{\isacharat}{\isamath{@}}%
 \renewcommand{\isacharbrackleft}{\isamath{[}}%
+\renewcommand{\isacharbackslash}{\isamath{\backslash}}%
 \renewcommand{\isacharbrackright}{\isamath{]}}%
 \renewcommand{\isacharunderscore}{\mbox{-}}%
 \renewcommand{\isacharbraceleft}{\isamath{\{}}%
@@ -154,3 +164,28 @@
 \renewcommand{\isastyleminor}{\sl}%
 \renewcommand{\isastylescript}{\footnotesize\sl}%
 }
+
+
+% tagged regions
+
+%plain TeX version of comment package -- much faster!
+\let\isafmtname\fmtname\def\fmtname{plain}
+\usepackage{comment}
+\let\fmtname\isafmtname
+
+\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
+
+\newcommand{\isakeeptag}[1]%
+{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
+\newcommand{\isadroptag}[1]%
+{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
+\newcommand{\isafoldtag}[1]%
+{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
+
+\isakeeptag{theory}
+\isakeeptag{proof}
+\isakeeptag{ML}
+\isakeeptag{visible}
+\isadroptag{invisible}
+
+\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}

--- a/doc-src/AxClass/generated/isabellesym.sty	Fri Aug 19 22:25:21 2005 +0200
+++ b/doc-src/AxClass/generated/isabellesym.sty	Fri Aug 19 22:28:23 2005 +0200
@@ -3,19 +3,20 @@
 %%
 %% definitions of standard Isabelle symbols
 %%
+%% $Id$
 
 % symbol definitions
 
-\newcommand{\isasymzero}{\isatext{\textzerooldstyle}}  %requires textcomp
-\newcommand{\isasymone}{\isatext{\textoneoldstyle}}  %requires textcomp
-\newcommand{\isasymtwo}{\isatext{\texttwooldstyle}}  %requires textcomp
-\newcommand{\isasymthree}{\isatext{\textthreeoldstyle}}  %requires textcomp
-\newcommand{\isasymfour}{\isatext{\textfouroldstyle}}  %requires textcomp
-\newcommand{\isasymfive}{\isatext{\textfiveoldstyle}}  %requires textcomp
-\newcommand{\isasymsix}{\isatext{\textsixoldstyle}}  %requires textcomp
-\newcommand{\isasymseven}{\isatext{\textsevenoldstyle}}  %requires textcomp
-\newcommand{\isasymeight}{\isatext{\texteightoldstyle}}  %requires textcomp
-\newcommand{\isasymnine}{\isatext{\textnineoldstyle}}  %requires textcomp
+\newcommand{\isasymzero}{\isamath{\mathbf{0}}}  %requires amssymb
+\newcommand{\isasymone}{\isamath{\mathbf{1}}}   %requires amssymb
+\newcommand{\isasymtwo}{\isamath{\mathbf{2}}}   %requires amssymb
+\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb
+\newcommand{\isasymfour}{\isamath{\mathbf{4}}}  %requires amssymb
+\newcommand{\isasymfive}{\isamath{\mathbf{5}}}  %requires amssymb
+\newcommand{\isasymsix}{\isamath{\mathbf{6}}}   %requires amssymb
+\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb
+\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb
+\newcommand{\isasymnine}{\isamath{\mathbf{9}}}  %requires amssymb
 \newcommand{\isasymA}{\isamath{\mathcal{A}}}
 \newcommand{\isasymB}{\isamath{\mathcal{B}}}
 \newcommand{\isasymC}{\isamath{\mathcal{C}}}
@@ -183,7 +184,12 @@
 \newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
 \newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
 \newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
-\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires latexsym
+\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}}  %requires amssymb
+\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}}  %requires amssymb
+\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}}  %requires amssymb
+\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}}  %requires amssymb
+\newcommand{\isasymrestriction}{\isamath{\restriction}}  %requires amssymb
+\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires amssymb
 \newcommand{\isasymup}{\isamath{\uparrow}}
 \newcommand{\isasymUp}{\isamath{\Uparrow}}
 \newcommand{\isasymdown}{\isamath{\downarrow}}
@@ -202,8 +208,8 @@
 \newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
 \newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
 \newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
-\newcommand{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel
-\newcommand{\isasymguillemotright}{\isatext{\frqq}}  %requires babel
+\newcommand{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel 
+\newcommand{\isasymguillemotright}{\isatext{\frqq}}  %requires babel 
 \newcommand{\isasymColon}{\isamath{\mathrel{::}}}
 \newcommand{\isasymnot}{\isamath{\neg}}
 \newcommand{\isasymbottom}{\isamath{\bot}}
@@ -214,8 +220,9 @@
 \newcommand{\isasymOr}{\isamath{\bigvee}}
 \newcommand{\isasymforall}{\isamath{\forall\,}}
 \newcommand{\isasymexists}{\isamath{\exists\,}}
-\newcommand{\isasymbox}{\isamath{\Box}}  %requires latexsym
-\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires latexsym
+\newcommand{\isasymnexists}{\isamath{\nexists\,}}  %requires amssymb
+\newcommand{\isasymbox}{\isamath{\Box}}  %requires amssymb
+\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssymb
 \newcommand{\isasymturnstile}{\isamath{\vdash}}
 \newcommand{\isasymTurnstile}{\isamath{\models}}
 \newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
@@ -236,8 +243,8 @@
 \newcommand{\isasymsupset}{\isamath{\supset}}
 \newcommand{\isasymsubseteq}{\isamath{\subseteq}}
 \newcommand{\isasymsupseteq}{\isamath{\supseteq}}
-\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}
-\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires latexsym
+\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}  %requires amssymb
+\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires amssymb
 \newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
 \newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
 \newcommand{\isasyminter}{\isamath{\cap}}
@@ -247,7 +254,7 @@
 \newcommand{\isasymsqunion}{\isamath{\sqcup}}
 \newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
 \newcommand{\isasymsqinter}{\isamath{\sqcap}}
-\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires stmaryrd
+\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires amsmath
 \newcommand{\isasymuplus}{\isamath{\uplus}}
 \newcommand{\isasymUplus}{\isamath{\biguplus\,}}
 \newcommand{\isasymnoteq}{\isamath{\not=}}
@@ -261,6 +268,8 @@
 \newcommand{\isasymequiv}{\isamath{\equiv}}
 \newcommand{\isasymfrown}{\isamath{\frown}}
 \newcommand{\isasympropto}{\isamath{\propto}}
+\newcommand{\isasymsome}{\isamath{\epsilon\,}}
+\newcommand{\isasymJoin}{\isamath{\Join}}  %requires amssymb
 \newcommand{\isasymbowtie}{\isamath{\bowtie}}
 \newcommand{\isasymprec}{\isamath{\prec}}
 \newcommand{\isasymsucc}{\isamath{\succ}}
@@ -278,10 +287,10 @@
 \newcommand{\isasymcirc}{\isamath{\circ}}
 \newcommand{\isasymdagger}{\isamath{\dagger}}
 \newcommand{\isasymddagger}{\isamath{\ddagger}}
-\newcommand{\isasymlhd}{\isamath{\lhd}}
-\newcommand{\isasymrhd}{\isamath{\rhd}}
-\newcommand{\isasymunlhd}{\isamath{\unlhd}}
-\newcommand{\isasymunrhd}{\isamath{\unrhd}}
+\newcommand{\isasymlhd}{\isamath{\lhd}}  %requires amssymb
+\newcommand{\isasymrhd}{\isamath{\rhd}}  %requires amssymb
+\newcommand{\isasymunlhd}{\isamath{\unlhd}}  %requires amssymb
+\newcommand{\isasymunrhd}{\isamath{\unrhd}}  %requires amssymb
 \newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
 \newcommand{\isasymtriangleright}{\isamath{\triangleright}}
 \newcommand{\isasymtriangle}{\isamath{\triangle}}
@@ -332,16 +341,15 @@
 \newcommand{\isasymparagraph}{\isatext{\rm\P}}
 \newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
 \newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
-\newcommand{\isasymeuro}{\isatext{\EUR}}  %requires marvosym
+\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}}  %requires greek babel
 \newcommand{\isasympounds}{\isamath{\pounds}}
 \newcommand{\isasymyen}{\isatext{\yen}}  %requires amssymb
-\newcommand{\isasymcent}{\isatext{\cent}}  %requires wasysym
-\newcommand{\isasymcurrency}{\isatext{\currency}}  %requires wasysym
+\newcommand{\isasymcent}{\isatext{\textcent}}  %requires textcomp
+\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
 \newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires latin1
 \newcommand{\isasymamalg}{\isamath{\amalg}}
-\newcommand{\isasymmho}{\isamath{\mho}}  %requires latexsym
-\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssym
-\newcommand{\isasymJoin}{\isamath{\Join}}  %requires latexsym
+\newcommand{\isasymmho}{\isamath{\mho}}  %requires amssymb
+\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssymb
 \newcommand{\isasymwp}{\isamath{\wp}}
 \newcommand{\isasymwrong}{\isamath{\wr}}
 \newcommand{\isasymstruct}{\isamath{\diamond}}
@@ -351,3 +359,4 @@
 \newcommand{\isasymcedilla}{\isatext{\c\relax}}
 \newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
 \newcommand{\isasymspacespace}{\isamath{~~}}
+\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}