# HG changeset patch
# User wenzelm
# Date 1124483303 -7200
# Node ID 153fe83804c93e8c56fe477646c482ecc6a9329b
# Parent  13c7d9c8557d59155cce51a63b79cb29e35af3cd
updated;

diff -r 13c7d9c8557d -r 153fe83804c9 doc-src/AxClass/generated/Group.tex
--- a/doc-src/AxClass/generated/Group.tex	Fri Aug 19 22:28:23 2005 +0200
+++ b/doc-src/AxClass/generated/Group.tex	Fri Aug 19 22:28:23 2005 +0200
@@ -1,11 +1,25 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Group}%
+\isamarkuptrue%
 %
 \isamarkupheader{Basic group theory%
 }
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isamarkupfalse%
+\isacommand{theory}\ Group\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
 \isamarkuptrue%
-\isacommand{theory}\ Group\ {\isacharequal}\ Main{\isacharcolon}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \medskip\noindent The meta-level type system of Isabelle supports
@@ -26,11 +40,11 @@
 First we declare some polymorphic constants required later for the
   signature parts of our structures.%
 \end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
 \isacommand{consts}\isanewline
 \ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
 \ \ invers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
-\ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymone}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
+\ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymone}{\isachardoublequote}{\isacharparenright}\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \noindent Next we define class \isa{monoid} of monoids with
@@ -38,11 +52,11 @@
   axioms are allowed for user convenience --- they simply represent
   the conjunction of their respective universal closures.%
 \end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
 \isacommand{axclass}\ monoid\ {\isasymsubseteq}\ type\isanewline
 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
-\ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse%
+\ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequote}\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \noindent So class \isa{monoid} contains exactly those types
@@ -59,7 +73,7 @@
   that the names of class axioms are automatically qualified with each
   class name, so we may re-use common names such as \isa{assoc}.%
 \end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
 \isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ type\isanewline
 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
 \isanewline
@@ -70,7 +84,7 @@
 \isanewline
 \isamarkupfalse%
 \isacommand{axclass}\ agroup\ {\isasymsubseteq}\ group\isanewline
-\ \ commute{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequote}\isamarkupfalse%
+\ \ commute{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequote}\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \noindent Class \isa{group} inherits associativity of \isa{{\isasymodot}}
@@ -97,8 +111,14 @@
   ``abstract theorems''.  For example, we may now derive the following
   well-known laws of general groups.%
 \end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
 \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
 \isamarkupfalse%
 \isacommand{proof}\ {\isacharminus}\isanewline
 \ \ \isamarkupfalse%
@@ -145,14 +165,27 @@
 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
 \isacommand{{\isachardot}}\isanewline
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isacommand{qed}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established
   much easier.%
 \end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
 \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
 \isamarkupfalse%
 \isacommand{proof}\ {\isacharminus}\isanewline
 \ \ \isamarkupfalse%
@@ -179,7 +212,14 @@
 \isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
 \isacommand{{\isachardot}}\isanewline
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isacommand{qed}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \medskip Abstract theorems may be instantiated to only those types
@@ -227,8 +267,14 @@
    \end{center}
  \end{figure}%
 \end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
 \isacommand{instance}\ monoid\ {\isasymsubseteq}\ semigroup\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
 \isamarkupfalse%
 \isacommand{proof}\isanewline
 \ \ \isamarkupfalse%
@@ -238,10 +284,23 @@
 \ \ \ \ \isamarkupfalse%
 \isacommand{by}\ {\isacharparenleft}rule\ monoid{\isachardot}assoc{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{qed}\isanewline
+\isacommand{qed}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
 \isanewline
 \isamarkupfalse%
 \isacommand{instance}\ group\ {\isasymsubseteq}\ monoid\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
 \isamarkupfalse%
 \isacommand{proof}\isanewline
 \ \ \isamarkupfalse%
@@ -259,7 +318,14 @@
 \ \ \ \ \isamarkupfalse%
 \isacommand{by}\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isacommand{qed}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \medskip The $\INSTANCE$ command sets up an appropriate goal that
@@ -291,11 +357,11 @@
   exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and
   \isa{False} as \isa{{\isasymone}} forms an Abelian group.%
 \end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
 \ \ times{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ inverse{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequote}\isanewline
-\ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymequiv}\ False{\isachardoublequote}\isamarkupfalse%
+\ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymequiv}\ False{\isachardoublequote}\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \medskip It is important to note that above $\DEFS$ are just
@@ -311,8 +377,14 @@
   operations on type \isa{bool} appropriately, the class membership
   \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.%
 \end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
 \isamarkupfalse%
 \isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\isanewline
 \ \ \ \ unfold\ times{\isacharunderscore}bool{\isacharunderscore}def\ inverse{\isacharunderscore}bool{\isacharunderscore}def\ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline
@@ -331,7 +403,14 @@
 \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
 \isacommand{by}\ blast\isanewline
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isacommand{qed}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 The result of an $\INSTANCE$ statement is both expressed as a
@@ -365,17 +444,23 @@
   products, direct sums or function spaces.  Subsequently we lift
   \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.%
 \end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-\ \ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}p\ {\isasymodot}\ q\ {\isasymequiv}\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\ \ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}p\ {\isasymodot}\ q\ {\isasymequiv}\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 It is very easy to see that associativity of \isa{{\isasymodot}} on \isa{{\isacharprime}a}
   and \isa{{\isasymodot}} on \isa{{\isacharprime}b} transfers to \isa{{\isasymodot}} on \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.  Hence the binary type constructor \isa{{\isasymodot}} maps semigroups
   to semigroups.  This may be established formally as follows.%
 \end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
 \isacommand{instance}\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
 \isamarkupfalse%
 \isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline
 \ \ \isamarkupfalse%
@@ -389,7 +474,14 @@
 \ \ \ \ \isamarkupfalse%
 \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
+\isacommand{qed}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 Thus, if we view class instances as ``structures'', then overloaded
@@ -397,9 +489,21 @@
   some kind of ``functors'' --- i.e.\ mappings between abstract
   theories.%
 \end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{end}\isanewline
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
 \isamarkupfalse%
+\isacommand{end}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
diff -r 13c7d9c8557d -r 153fe83804c9 doc-src/AxClass/generated/NatClass.tex
--- a/doc-src/AxClass/generated/NatClass.tex	Fri Aug 19 22:28:23 2005 +0200
+++ b/doc-src/AxClass/generated/NatClass.tex	Fri Aug 19 22:28:23 2005 +0200
@@ -1,11 +1,25 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{NatClass}%
+\isamarkuptrue%
 %
 \isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}%
 }
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isamarkupfalse%
+\isacommand{theory}\ NatClass\ \isakeyword{imports}\ FOL\ \isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
 \isamarkuptrue%
-\isacommand{theory}\ NatClass\ {\isacharequal}\ FOL{\isacharcolon}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \medskip\noindent Axiomatic type classes abstract over exactly one
@@ -17,7 +31,7 @@
  Isabelle/FOL.\footnote{See also
  \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}%
 \end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
 \isacommand{consts}\isanewline
 \ \ zero\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymzero}{\isachardoublequote}{\isacharparenright}\isanewline
 \ \ Suc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
@@ -34,7 +48,7 @@
 \isamarkupfalse%
 \isacommand{constdefs}\isanewline
 \ \ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isacharcolon}{\isacharcolon}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ {\isachardoublequote}m\ {\isacharplus}\ n\ {\isasymequiv}\ rec{\isacharparenleft}m{\isacharcomma}\ n{\isacharcomma}\ {\isasymlambda}x\ y{\isachardot}\ Suc{\isacharparenleft}y{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\ \ {\isachardoublequote}m\ {\isacharplus}\ n\ {\isasymequiv}\ rec{\isacharparenleft}m{\isacharcomma}\ n{\isacharcomma}\ {\isasymlambda}x\ y{\isachardot}\ Suc{\isacharparenleft}y{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 This is an abstract version of the plain \isa{Nat} theory in
@@ -61,8 +75,20 @@
  re-used with some trivial changes only (mostly adding some type
  constraints).%
 \end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{end}\isamarkupfalse%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isamarkupfalse%
+\isacommand{end}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
diff -r 13c7d9c8557d -r 153fe83804c9 doc-src/AxClass/generated/Product.tex
--- a/doc-src/AxClass/generated/Product.tex	Fri Aug 19 22:28:23 2005 +0200
+++ b/doc-src/AxClass/generated/Product.tex	Fri Aug 19 22:28:23 2005 +0200
@@ -1,11 +1,25 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Product}%
+\isamarkuptrue%
 %
 \isamarkupheader{Syntactic classes%
 }
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isamarkupfalse%
+\isacommand{theory}\ Product\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
 \isamarkuptrue%
-\isacommand{theory}\ Product\ {\isacharequal}\ Main{\isacharcolon}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \medskip\noindent There is still a feature of Isabelle's type system
@@ -20,12 +34,12 @@
  The \isa{product} class below provides a less degenerate example of
  syntactic type classes.%
 \end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
 \isacommand{axclass}\isanewline
 \ \ product\ {\isasymsubseteq}\ type\isanewline
 \isamarkupfalse%
 \isacommand{consts}\isanewline
-\ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
+\ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 Here class \isa{product} is defined as subclass of \isa{type}
@@ -53,12 +67,25 @@
   This is done for class \isa{product} and type \isa{bool} as
   follows.%
 \end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product\ \isamarkupfalse%
-\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isamarkupfalse%
+\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
 \isamarkupfalse%
 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-\ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}\isamarkupfalse%
+\ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 The definition \isa{prod{\isacharunderscore}bool{\isacharunderscore}def} becomes syntactically
@@ -83,9 +110,21 @@
  Isabelle's meta-logic, because there is no internal notion of
  ``providing operations'' or even ``names of functions''.%
 \end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{end}\isanewline
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
 \isamarkupfalse%
+\isacommand{end}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
diff -r 13c7d9c8557d -r 153fe83804c9 doc-src/AxClass/generated/Semigroups.tex
--- a/doc-src/AxClass/generated/Semigroups.tex	Fri Aug 19 22:28:23 2005 +0200
+++ b/doc-src/AxClass/generated/Semigroups.tex	Fri Aug 19 22:28:23 2005 +0200
@@ -1,11 +1,25 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Semigroups}%
+\isamarkuptrue%
 %
 \isamarkupheader{Semigroups%
 }
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isamarkupfalse%
+\isacommand{theory}\ Semigroups\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
 \isamarkuptrue%
-\isacommand{theory}\ Semigroups\ {\isacharequal}\ Main{\isacharcolon}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \medskip\noindent An axiomatic type class is simply a class of types
@@ -19,12 +33,12 @@
   We illustrate these basic concepts by the following formulation of
   semigroups.%
 \end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
 \isacommand{consts}\isanewline
 \ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
 \isamarkupfalse%
 \isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ type\isanewline
-\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \noindent Above we have first declared a polymorphic constant \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and then defined the class \isa{semigroup} of
@@ -41,20 +55,32 @@
   Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}\isactrlsup {\isasymtau}{\isacharparenright}}, while the original \isa{semigroup} would
   correspond to semigroups of the form \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}\isactrlsup {\isasymtau}{\isacharparenright}}.%
 \end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
 \isacommand{consts}\isanewline
 \ \ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
 \isamarkupfalse%
 \isacommand{axclass}\ plus{\isacharunderscore}semigroup\ {\isasymsubseteq}\ type\isanewline
-\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \noindent Even if classes \isa{plus{\isacharunderscore}semigroup} and \isa{semigroup} both represent semigroups in a sense, they are certainly
   not quite the same.%
 \end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{end}\isanewline
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
 \isamarkupfalse%
+\isacommand{end}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
diff -r 13c7d9c8557d -r 153fe83804c9 doc-src/AxClass/generated/isabelle.sty
--- a/doc-src/AxClass/generated/isabelle.sty	Fri Aug 19 22:28:23 2005 +0200
+++ b/doc-src/AxClass/generated/isabelle.sty	Fri Aug 19 22:28:23 2005 +0200
@@ -3,7 +3,7 @@
 %%
 %% macros for Isabelle generated LaTeX output
 %%
-%% $Id$
+%% 
 
 %%% Simple document preparation (based on theory token language and symbols)
 
diff -r 13c7d9c8557d -r 153fe83804c9 doc-src/AxClass/generated/isabellesym.sty
--- a/doc-src/AxClass/generated/isabellesym.sty	Fri Aug 19 22:28:23 2005 +0200
+++ b/doc-src/AxClass/generated/isabellesym.sty	Fri Aug 19 22:28:23 2005 +0200
@@ -3,7 +3,7 @@
 %%
 %% definitions of standard Isabelle symbols
 %%
-%% $Id$
+%% 
 
 % symbol definitions