updated;

--- a/doc-src/AxClass/generated/Group.tex	Fri Aug 04 10:59:22 2000 +0200
+++ b/doc-src/AxClass/generated/Group.tex	Fri Aug 04 10:59:28 2000 +0200
@@ -1,7 +1,7 @@
 \begin{isabelle}%
 %
 \isamarkupheader{Basic group theory}
-\isacommand{theory}~Group~=~Main:%
+\isacommand{theory}\ Group\ =\ Main:%
 \begin{isamarkuptext}%
 \medskip\noindent The meta-type system of Isabelle supports
  \emph{intersections} and \emph{inclusions} of type classes. These
@@ -19,9 +19,9 @@
  signature parts of our structures.%
 \end{isamarkuptext}%
 \isacommand{consts}\isanewline
-~~times~::~{"}'a~=>~'a~=>~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)\isanewline
-~~inverse~::~{"}'a~=>~'a{"}~~~~~~~~({"}(\_{\isasyminv}){"}~[1000]~999)\isanewline
-~~one~::~'a~~~~~~~~~~~~~~~~~~~~({"}{\isasymunit}{"})%
+\ \ times\ ::\ {"}'a\ =>\ 'a\ =>\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOtimes}{"}\ 70)\isanewline
+\ \ inverse\ ::\ {"}'a\ =>\ 'a{"}\ \ \ \ \ \ \ \ ({"}(\_{\isasyminv}){"}\ [1000]\ 999)\isanewline
+\ \ one\ ::\ 'a\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ ({"}{\isasymunit}{"})%
 \begin{isamarkuptext}%
 \noindent Next we define class $monoid$ of monoids with operations
  $\TIMES$ and $1$.  Note that multiple class axioms are allowed for
@@ -29,15 +29,15 @@
  respective universal closures.%
 \end{isamarkuptext}%
 \isacommand{axclass}\isanewline
-~~monoid~<~{"}term{"}\isanewline
-~~assoc:~~~~~~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
-~~left\_unit:~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
-~~right\_unit:~{"}x~{\isasymOtimes}~{\isasymunit}~=~x{"}%
+\ \ monoid\ <\ {"}term{"}\isanewline
+\ \ assoc:\ \ \ \ \ \ {"}(x\ {\isasymOtimes}\ y)\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline
+\ \ left\_unit:\ \ {"}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{"}\isanewline
+\ \ right\_unit:\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{"}%
 \begin{isamarkuptext}%
 \noindent So class $monoid$ contains exactly those types $\tau$ where
  $\TIMES :: \tau \To \tau \To \tau$ and $1 :: \tau$ are specified
  appropriately, such that $\TIMES$ is associative and $1$ is a left
- and right unit element for $\TIMES$.%
+ and right unit element for the $\TIMES$ operation.%
 \end{isamarkuptext}%
 %
 \begin{isamarkuptext}%
@@ -47,17 +47,17 @@
  name, so we may re-use common names such as $assoc$.%
 \end{isamarkuptext}%
 \isacommand{axclass}\isanewline
-~~semigroup~<~{"}term{"}\isanewline
-~~assoc:~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
+\ \ semigroup\ <\ {"}term{"}\isanewline
+\ \ assoc:\ {"}(x\ {\isasymOtimes}\ y)\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline
 \isanewline
 \isacommand{axclass}\isanewline
-~~group~<~semigroup\isanewline
-~~left\_unit:~~~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
-~~left\_inverse:~{"}x{\isasyminv}~{\isasymOtimes}~x~=~{\isasymunit}{"}\isanewline
+\ \ group\ <\ semigroup\isanewline
+\ \ left\_unit:\ \ \ \ {"}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{"}\isanewline
+\ \ left\_inverse:\ {"}x{\isasyminv}\ {\isasymOtimes}\ x\ =\ {\isasymunit}{"}\isanewline
 \isanewline
 \isacommand{axclass}\isanewline
-~~agroup~<~group\isanewline
-~~commute:~{"}x~{\isasymOtimes}~y~=~y~{\isasymOtimes}~x{"}%
+\ \ agroup\ <\ group\isanewline
+\ \ commute:\ {"}x\ {\isasymOtimes}\ y\ =\ y\ {\isasymOtimes}\ x{"}%
 \begin{isamarkuptext}%
 \noindent Class $group$ inherits associativity of $\TIMES$ from
  $semigroup$ and adds two further group axioms. Similarly, $agroup$
@@ -85,42 +85,42 @@
  ``abstract theorems''.  For example, we may now derive the following
  well-known laws of general groups.%
 \end{isamarkuptext}%
-\isacommand{theorem}~group\_right\_inverse:~{"}x~{\isasymOtimes}~x{\isasyminv}~=~({\isasymunit}{\isasymColon}'a{\isasymColon}group){"}\isanewline
-\isacommand{proof}~-\isanewline
-~~\isacommand{have}~{"}x~{\isasymOtimes}~x{\isasyminv}~=~{\isasymunit}~{\isasymOtimes}~(x~{\isasymOtimes}~x{\isasyminv}){"}\isanewline
-~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}~{\isasymOtimes}~x~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~x{\isasyminv}~{\isasymOtimes}~x~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~(x{\isasyminv}~{\isasymOtimes}~x)~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~{\isasymunit}~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~({\isasymunit}~{\isasymOtimes}~x{\isasyminv}){"}\isanewline
-~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
-~~\isacommand{finally}~\isacommand{show}~?thesis~\isacommand{.}\isanewline
+\isacommand{theorem}\ group\_right\_inverse:\ {"}x\ {\isasymOtimes}\ x{\isasyminv}\ =\ ({\isasymunit}{\isasymColon}'a{\isasymColon}group){"}\isanewline
+\isacommand{proof}\ -\isanewline
+\ \ \isacommand{have}\ {"}x\ {\isasymOtimes}\ x{\isasyminv}\ =\ {\isasymunit}\ {\isasymOtimes}\ (x\ {\isasymOtimes}\ x{\isasyminv}){"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_unit)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ (x{\isasyminv}\ {\isasymOtimes}\ x)\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ {\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ ({\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}){"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_unit)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ {\isasymunit}{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline
+\ \ \isacommand{finally}\ \isacommand{show}\ ?thesis\ \isacommand{.}\isanewline
 \isacommand{qed}%
 \begin{isamarkuptext}%
 \noindent With $group_right_inverse$ already available,
  $group_right_unit$\label{thm:group-right-unit} is now established
  much easier.%
 \end{isamarkuptext}%
-\isacommand{theorem}~group\_right\_unit:~{"}x~{\isasymOtimes}~{\isasymunit}~=~(x{\isasymColon}'a{\isasymColon}group){"}\isanewline
-\isacommand{proof}~-\isanewline
-~~\isacommand{have}~{"}x~{\isasymOtimes}~{\isasymunit}~=~x~{\isasymOtimes}~(x{\isasyminv}~{\isasymOtimes}~x){"}\isanewline
-~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~x~{\isasymOtimes}~x{\isasyminv}~{\isasymOtimes}~x{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}~{\isasymOtimes}~x{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~group\_right\_inverse)\isanewline
-~~\isacommand{also}~\isacommand{have}~{"}...~=~x{"}\isanewline
-~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline
-~~\isacommand{finally}~\isacommand{show}~?thesis~\isacommand{.}\isanewline
+\isacommand{theorem}\ group\_right\_unit:\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ (x{\isasymColon}'a{\isasymColon}group){"}\isanewline
+\isacommand{proof}\ -\isanewline
+\ \ \isacommand{have}\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x\ {\isasymOtimes}\ (x{\isasyminv}\ {\isasymOtimes}\ x){"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ x\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ group\_right\_inverse)\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ x{"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_unit)\isanewline
+\ \ \isacommand{finally}\ \isacommand{show}\ ?thesis\ \isacommand{.}\isanewline
 \isacommand{qed}%
 \begin{isamarkuptext}%
 \medskip Abstract theorems may be instantiated to only those types
@@ -169,22 +169,22 @@
    \end{center}
  \end{figure}%
 \end{isamarkuptext}%
-\isacommand{instance}~monoid~<~semigroup\isanewline
-\isacommand{proof}~intro\_classes\isanewline
-~~\isacommand{fix}~x~y~z~::~{"}'a{\isasymColon}monoid{"}\isanewline
-~~\isacommand{show}~{"}x~{\isasymOtimes}~y~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
-~~~~\isacommand{by}~(rule~monoid.assoc)\isanewline
+\isacommand{instance}\ monoid\ <\ semigroup\isanewline
+\isacommand{proof}\ intro\_classes\isanewline
+\ \ \isacommand{fix}\ x\ y\ z\ ::\ {"}'a{\isasymColon}monoid{"}\isanewline
+\ \ \isacommand{show}\ {"}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline
+\ \ \ \ \isacommand{by}\ (rule\ monoid.assoc)\isanewline
 \isacommand{qed}\isanewline
 \isanewline
-\isacommand{instance}~group~<~monoid\isanewline
-\isacommand{proof}~intro\_classes\isanewline
-~~\isacommand{fix}~x~y~z~::~{"}'a{\isasymColon}group{"}\isanewline
-~~\isacommand{show}~{"}x~{\isasymOtimes}~y~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
-~~~~\isacommand{by}~(rule~semigroup.assoc)\isanewline
-~~\isacommand{show}~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
-~~~~\isacommand{by}~(rule~group.left\_unit)\isanewline
-~~\isacommand{show}~{"}x~{\isasymOtimes}~{\isasymunit}~=~x{"}\isanewline
-~~~~\isacommand{by}~(rule~group\_right\_unit)\isanewline
+\isacommand{instance}\ group\ <\ monoid\isanewline
+\isacommand{proof}\ intro\_classes\isanewline
+\ \ \isacommand{fix}\ x\ y\ z\ ::\ {"}'a{\isasymColon}group{"}\isanewline
+\ \ \isacommand{show}\ {"}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline
+\ \ \ \ \isacommand{by}\ (rule\ semigroup.assoc)\isanewline
+\ \ \isacommand{show}\ {"}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{"}\isanewline
+\ \ \ \ \isacommand{by}\ (rule\ group.left\_unit)\isanewline
+\ \ \isacommand{show}\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{"}\isanewline
+\ \ \ \ \isacommand{by}\ (rule\ group\_right\_unit)\isanewline
 \isacommand{qed}%
 \begin{isamarkuptext}%
 \medskip The $\isakeyword{instance}$ command sets up an appropriate
@@ -211,13 +211,13 @@
  transferred to Isabelle's type signature level.
 
  \medskip As a typical example, we show that type $bool$ with
- exclusive-or as operation $\TIMES$, identity as $\isasyminv$, and
+ exclusive-or as $\TIMES$ operation, identity as $\isasyminv$, and
  $False$ as $1$ forms an Abelian group.%
 \end{isamarkuptext}%
-\isacommand{defs}~(\isakeyword{overloaded})\isanewline
-~~times\_bool\_def:~~~{"}x~{\isasymOtimes}~y~{\isasymequiv}~x~{\isasymnoteq}~(y{\isasymColon}bool){"}\isanewline
-~~inverse\_bool\_def:~{"}x{\isasyminv}~{\isasymequiv}~x{\isasymColon}bool{"}\isanewline
-~~unit\_bool\_def:~~~~{"}{\isasymunit}~{\isasymequiv}~False{"}%
+\isacommand{defs}\ (\isakeyword{overloaded})\isanewline
+\ \ times\_bool\_def:\ \ \ {"}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ (y{\isasymColon}bool){"}\isanewline
+\ \ inverse\_bool\_def:\ {"}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{"}\isanewline
+\ \ unit\_bool\_def:\ \ \ \ {"}{\isasymunit}\ {\isasymequiv}\ False{"}%
 \begin{isamarkuptext}%
 \medskip It is important to note that above $\DEFS$ are just
  overloaded meta-level constant definitions, where type classes are
@@ -232,14 +232,14 @@
  operations on type $bool$ appropriately, the class membership $bool
  :: agroup$ may be now derived as follows.%
 \end{isamarkuptext}%
-\isacommand{instance}~bool~::~agroup\isanewline
-\isacommand{proof}~(intro\_classes,\isanewline
-~~~~unfold~times\_bool\_def~inverse\_bool\_def~unit\_bool\_def)\isanewline
-~~\isacommand{fix}~x~y~z\isanewline
-~~\isacommand{show}~{"}((x~{\isasymnoteq}~y)~{\isasymnoteq}~z)~=~(x~{\isasymnoteq}~(y~{\isasymnoteq}~z)){"}~\isacommand{by}~blast\isanewline
-~~\isacommand{show}~{"}(False~{\isasymnoteq}~x)~=~x{"}~\isacommand{by}~blast\isanewline
-~~\isacommand{show}~{"}(x~{\isasymnoteq}~x)~=~False{"}~\isacommand{by}~blast\isanewline
-~~\isacommand{show}~{"}(x~{\isasymnoteq}~y)~=~(y~{\isasymnoteq}~x){"}~\isacommand{by}~blast\isanewline
+\isacommand{instance}\ bool\ ::\ agroup\isanewline
+\isacommand{proof}\ (intro\_classes,\isanewline
+\ \ \ \ unfold\ times\_bool\_def\ inverse\_bool\_def\ unit\_bool\_def)\isanewline
+\ \ \isacommand{fix}\ x\ y\ z\isanewline
+\ \ \isacommand{show}\ {"}((x\ {\isasymnoteq}\ y)\ {\isasymnoteq}\ z)\ =\ (x\ {\isasymnoteq}\ (y\ {\isasymnoteq}\ z)){"}\ \isacommand{by}\ blast\isanewline
+\ \ \isacommand{show}\ {"}(False\ {\isasymnoteq}\ x)\ =\ x{"}\ \isacommand{by}\ blast\isanewline
+\ \ \isacommand{show}\ {"}(x\ {\isasymnoteq}\ x)\ =\ False{"}\ \isacommand{by}\ blast\isanewline
+\ \ \isacommand{show}\ {"}(x\ {\isasymnoteq}\ y)\ =\ (y\ {\isasymnoteq}\ x){"}\ \isacommand{by}\ blast\isanewline
 \isacommand{qed}%
 \begin{isamarkuptext}%
 The result of an $\isakeyword{instance}$ statement is both expressed
@@ -269,23 +269,23 @@
  products, direct sums or function spaces.  Subsequently we lift
  $\TIMES$ component-wise to binary products $\alpha \times \beta$.%
 \end{isamarkuptext}%
-\isacommand{defs}~(\isakeyword{overloaded})\isanewline
-~~times\_prod\_def:~{"}p~{\isasymOtimes}~q~{\isasymequiv}~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q){"}%
+\isacommand{defs}\ (\isakeyword{overloaded})\isanewline
+\ \ times\_prod\_def:\ {"}p\ {\isasymOtimes}\ q\ {\isasymequiv}\ (fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q){"}%
 \begin{isamarkuptext}%
 It is very easy to see that associativity of $\TIMES^\alpha$ and
  $\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$.  Hence
  the binary type constructor $\times$ maps semigroups to semigroups.
  This may be established formally as follows.%
 \end{isamarkuptext}%
-\isacommand{instance}~*~::~(semigroup,~semigroup)~semigroup\isanewline
-\isacommand{proof}~(intro\_classes,~unfold~times\_prod\_def)\isanewline
-~~\isacommand{fix}~p~q~r~::~{"}'a{\isasymColon}semigroup~{\isasymtimes}~'b{\isasymColon}semigroup{"}\isanewline
-~~\isacommand{show}\isanewline
-~~~~{"}(fst~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q)~{\isasymOtimes}~fst~r,\isanewline
-~~~~~~snd~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q)~{\isasymOtimes}~snd~r)~=\isanewline
-~~~~~~~(fst~p~{\isasymOtimes}~fst~(fst~q~{\isasymOtimes}~fst~r,~snd~q~{\isasymOtimes}~snd~r),\isanewline
-~~~~~~~~snd~p~{\isasymOtimes}~snd~(fst~q~{\isasymOtimes}~fst~r,~snd~q~{\isasymOtimes}~snd~r)){"}\isanewline
-~~~~\isacommand{by}~(simp~add:~semigroup.assoc)\isanewline
+\isacommand{instance}\ *\ ::\ (semigroup,\ semigroup)\ semigroup\isanewline
+\isacommand{proof}\ (intro\_classes,\ unfold\ times\_prod\_def)\isanewline
+\ \ \isacommand{fix}\ p\ q\ r\ ::\ {"}'a{\isasymColon}semigroup\ {\isasymtimes}\ 'b{\isasymColon}semigroup{"}\isanewline
+\ \ \isacommand{show}\isanewline
+\ \ \ \ {"}(fst\ (fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q)\ {\isasymOtimes}\ fst\ r,\isanewline
+\ \ \ \ \ \ snd\ (fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q)\ {\isasymOtimes}\ snd\ r)\ =\isanewline
+\ \ \ \ \ \ \ (fst\ p\ {\isasymOtimes}\ fst\ (fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r),\isanewline
+\ \ \ \ \ \ \ \ snd\ p\ {\isasymOtimes}\ snd\ (fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r)){"}\isanewline
+\ \ \ \ \isacommand{by}\ (simp\ add:\ semigroup.assoc)\isanewline
 \isacommand{qed}%
 \begin{isamarkuptext}%
 Thus, if we view class instances as ``structures'', then overloaded

--- a/doc-src/AxClass/generated/NatClass.tex	Fri Aug 04 10:59:22 2000 +0200
+++ b/doc-src/AxClass/generated/NatClass.tex	Fri Aug 04 10:59:28 2000 +0200
@@ -1,7 +1,7 @@
 \begin{isabelle}%
 %
 \isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}}
-\isacommand{theory}~NatClass~=~FOL:%
+\isacommand{theory}\ NatClass\ =\ FOL:%
 \begin{isamarkuptext}%
 \medskip\noindent Axiomatic type classes abstract over exactly one
  type argument. Thus, any \emph{axiomatic} theory extension where each
@@ -13,21 +13,21 @@
  \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}%
 \end{isamarkuptext}%
 \isacommand{consts}\isanewline
-~~zero~::~'a~~~~({"}0{"})\isanewline
-~~Suc~::~{"}'a~{\isasymRightarrow}~'a{"}\isanewline
-~~rec~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~('a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a)~{\isasymRightarrow}~'a{"}\isanewline
+\ \ zero\ ::\ 'a\ \ \ \ ({"}0{"})\isanewline
+\ \ Suc\ ::\ {"}'a\ {\isasymRightarrow}\ 'a{"}\isanewline
+\ \ rec\ ::\ {"}'a\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ ('a\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a)\ {\isasymRightarrow}\ 'a{"}\isanewline
 \isanewline
 \isacommand{axclass}\isanewline
-~~nat~<~{"}term{"}\isanewline
-~~induct:~~~~~{"}P(0)~{\isasymLongrightarrow}~({\isasymAnd}x.~P(x)~{\isasymLongrightarrow}~P(Suc(x)))~{\isasymLongrightarrow}~P(n){"}\isanewline
-~~Suc\_inject:~{"}Suc(m)~=~Suc(n)~{\isasymLongrightarrow}~m~=~n{"}\isanewline
-~~Suc\_neq\_0:~~{"}Suc(m)~=~0~{\isasymLongrightarrow}~R{"}\isanewline
-~~rec\_0:~~~~~~{"}rec(0,~a,~f)~=~a{"}\isanewline
-~~rec\_Suc:~~~~{"}rec(Suc(m),~a,~f)~=~f(m,~rec(m,~a,~f)){"}\isanewline
+\ \ nat\ <\ {"}term{"}\isanewline
+\ \ induct:\ \ \ \ \ {"}P(0)\ {\isasymLongrightarrow}\ ({\isasymAnd}x.\ P(x)\ {\isasymLongrightarrow}\ P(Suc(x)))\ {\isasymLongrightarrow}\ P(n){"}\isanewline
+\ \ Suc\_inject:\ {"}Suc(m)\ =\ Suc(n)\ {\isasymLongrightarrow}\ m\ =\ n{"}\isanewline
+\ \ Suc\_neq\_0:\ \ {"}Suc(m)\ =\ 0\ {\isasymLongrightarrow}\ R{"}\isanewline
+\ \ rec\_0:\ \ \ \ \ \ {"}rec(0,\ a,\ f)\ =\ a{"}\isanewline
+\ \ rec\_Suc:\ \ \ \ {"}rec(Suc(m),\ a,\ f)\ =\ f(m,\ rec(m,\ a,\ f)){"}\isanewline
 \isanewline
 \isacommand{constdefs}\isanewline
-~~add~::~{"}'a::nat~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}+{"}~60)\isanewline
-~~{"}m~+~n~{\isasymequiv}~rec(m,~n,~{\isasymlambda}x~y.~Suc(y)){"}%
+\ \ add\ ::\ {"}'a::nat\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}+{"}\ 60)\isanewline
+\ \ {"}m\ +\ n\ {\isasymequiv}\ rec(m,\ n,\ {\isasymlambda}x\ y.\ Suc(y)){"}%
 \begin{isamarkuptext}%
 This is an abstract version of the plain $Nat$ theory in
  FOL.\footnote{See

--- a/doc-src/AxClass/generated/Product.tex	Fri Aug 04 10:59:22 2000 +0200
+++ b/doc-src/AxClass/generated/Product.tex	Fri Aug 04 10:59:28 2000 +0200
@@ -1,7 +1,7 @@
 \begin{isabelle}%
 %
 \isamarkupheader{Syntactic classes}
-\isacommand{theory}~Product~=~Main:%
+\isacommand{theory}\ Product\ =\ Main:%
 \begin{isamarkuptext}%
 \medskip\noindent There is still a feature of Isabelle's type system
  left that we have not yet discussed.  When declaring polymorphic
@@ -17,9 +17,9 @@
  syntactic type classes.%
 \end{isamarkuptext}%
 \isacommand{axclass}\isanewline
-~~product~<~{"}term{"}\isanewline
+\ \ product\ <\ {"}term{"}\isanewline
 \isacommand{consts}\isanewline
-~~product~::~{"}'a::product~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)%
+\ \ product\ ::\ {"}'a::product\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOtimes}{"}\ 70)%
 \begin{isamarkuptext}%
 Here class $product$ is defined as subclass of $term$ without any
  additional axioms.  This effects in logical equivalence of $product$
@@ -48,10 +48,10 @@
 
  This is done for class $product$ and type $bool$ as follows.%
 \end{isamarkuptext}%
-\isacommand{instance}~bool~::~product\isanewline
-~~\isacommand{by}~intro\_classes\isanewline
-\isacommand{defs}~(\isakeyword{overloaded})\isanewline
-~~product\_bool\_def:~{"}x~{\isasymOtimes}~y~{\isasymequiv}~x~{\isasymand}~y{"}%
+\isacommand{instance}\ bool\ ::\ product\isanewline
+\ \ \isacommand{by}\ intro\_classes\isanewline
+\isacommand{defs}\ (\isakeyword{overloaded})\isanewline
+\ \ product\_bool\_def:\ {"}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{"}%
 \begin{isamarkuptext}%
 The definition $prod_bool_def$ becomes syntactically well-formed only
  after the arity $bool :: product$ is made known to the type checker.

--- a/doc-src/AxClass/generated/Semigroups.tex	Fri Aug 04 10:59:22 2000 +0200
+++ b/doc-src/AxClass/generated/Semigroups.tex	Fri Aug 04 10:59:28 2000 +0200
@@ -1,7 +1,7 @@
 \begin{isabelle}%
 %
 \isamarkupheader{Semigroups}
-\isacommand{theory}~Semigroups~=~Main:%
+\isacommand{theory}\ Semigroups\ =\ Main:%
 \begin{isamarkuptext}%
 \medskip\noindent An axiomatic type class is simply a class of types
  that all meet certain properties, which are also called \emph{class
@@ -15,10 +15,10 @@
  semigroups.%
 \end{isamarkuptext}%
 \isacommand{consts}\isanewline
-~~times~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)\isanewline
+\ \ times\ ::\ {"}'a\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOtimes}{"}\ 70)\isanewline
 \isacommand{axclass}\isanewline
-~~semigroup~<~{"}term{"}\isanewline
-~~assoc:~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}%
+\ \ semigroup\ <\ {"}term{"}\isanewline
+\ \ assoc:\ {"}(x\ {\isasymOtimes}\ y)\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}%
 \begin{isamarkuptext}%
 \noindent Above we have first declared a polymorphic constant $\TIMES
  :: \alpha \To \alpha \To \alpha$ and then defined the class
@@ -37,10 +37,10 @@
  to semigroups $(\tau, \TIMES^\tau)$.%
 \end{isamarkuptext}%
 \isacommand{consts}\isanewline
-~~plus~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOplus}{"}~70)\isanewline
+\ \ plus\ ::\ {"}'a\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOplus}{"}\ 70)\isanewline
 \isacommand{axclass}\isanewline
-~~plus\_semigroup~<~{"}term{"}\isanewline
-~~assoc:~{"}(x~{\isasymOplus}~y)~{\isasymOplus}~z~=~x~{\isasymOplus}~(y~{\isasymOplus}~z){"}%
+\ \ plus\_semigroup\ <\ {"}term{"}\isanewline
+\ \ assoc:\ {"}(x\ {\isasymOplus}\ y)\ {\isasymOplus}\ z\ =\ x\ {\isasymOplus}\ (y\ {\isasymOplus}\ z){"}%
 \begin{isamarkuptext}%
 \noindent Even if classes $plus_semigroup$ and $semigroup$ both
  represent semigroups in a sense, they are certainly not quite the