updated;

--- a/doc-src/AxClass/generated/Group.tex	Sun Aug 20 17:45:20 2000 +0200
+++ b/doc-src/AxClass/generated/Group.tex	Mon Aug 21 13:47:24 2000 +0200
@@ -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\ ::\ {\isachardoublequote}{\isacharprime}a\ ={\isachargreater}\ {\isacharprime}a\ ={\isachargreater}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ 70{\isacharparenright}\isanewline
+\ \ inverse\ ::\ {\isachardoublequote}{\isacharprime}a\ ={\isachargreater}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}1000{\isacharbrackright}\ 999{\isacharparenright}\isanewline
+\ \ one\ ::\ {\isacharprime}a\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymunit}{\isachardoublequote}{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent Next we define class $monoid$ of monoids with operations
  $\TIMES$ and $1$.  Note that multiple class axioms are allowed for
@@ -29,10 +29,10 @@
  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\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\ \ assoc:\ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ left{\isacharunderscore}unit:\ \ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{\isachardoublequote}\isanewline
+\ \ right{\isacharunderscore}unit:\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent So class $monoid$ contains exactly those types $\tau$ where
  $\TIMES :: \tau \To \tau \To \tau$ and $1 :: \tau$ are specified
@@ -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\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\ \ assoc:\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
 \isanewline
 \isacommand{axclass}\isanewline
-\ \ group\ <\ semigroup\isanewline
-\ \ left\_unit:\ \ \ \ {"}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{"}\isanewline
-\ \ left\_inverse:\ {"}x{\isasyminv}\ {\isasymOtimes}\ x\ =\ {\isasymunit}{"}\isanewline
+\ \ group\ {\isacharless}\ semigroup\isanewline
+\ \ left{\isacharunderscore}unit:\ \ \ \ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{\isachardoublequote}\isanewline
+\ \ left{\isacharunderscore}inverse:\ {\isachardoublequote}x{\isasyminv}\ {\isasymOtimes}\ x\ =\ {\isasymunit}{\isachardoublequote}\isanewline
 \isanewline
 \isacommand{axclass}\isanewline
-\ \ agroup\ <\ group\isanewline
-\ \ commute:\ {"}x\ {\isasymOtimes}\ y\ =\ y\ {\isasymOtimes}\ x{"}%
+\ \ agroup\ {\isacharless}\ group\isanewline
+\ \ commute:\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ =\ y\ {\isasymOtimes}\ x{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent Class $group$ inherits associativity of $\TIMES$ from
  $semigroup$ and adds two further group axioms. Similarly, $agroup$
@@ -85,24 +85,24 @@
  ``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{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse:\ {\isachardoublequote}x\ {\isasymOtimes}\ x{\isasyminv}\ =\ {\isacharparenleft}{\isasymunit}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{proof}\ {\isacharminus}\isanewline
+\ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymOtimes}\ x{\isasyminv}\ =\ {\isasymunit}\ {\isasymOtimes}\ {\isacharparenleft}x\ {\isasymOtimes}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}unit{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ semigroup.assoc{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}inverse{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isacharparenleft}x{\isasyminv}\ {\isasymOtimes}\ x{\isacharparenright}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ semigroup.assoc{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}inverse{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isacharparenleft}{\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ semigroup.assoc{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}unit{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isasymunit}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}inverse{\isacharparenright}\isanewline
 \ \ \isacommand{finally}\ \isacommand{show}\ ?thesis\ \isacommand{.}\isanewline
 \isacommand{qed}%
 \begin{isamarkuptext}%
@@ -110,16 +110,16 @@
  $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{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit:\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ =\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{proof}\ {\isacharminus}\isanewline
+\ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}x{\isasyminv}\ {\isasymOtimes}\ x{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}inverse{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ x\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ semigroup.assoc{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}...\ =\ x{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only:\ group.left{\isacharunderscore}unit{\isacharparenright}\isanewline
 \ \ \isacommand{finally}\ \isacommand{show}\ ?thesis\ \isacommand{.}\isanewline
 \isacommand{qed}%
 \begin{isamarkuptext}%
@@ -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\ {\isacharless}\ semigroup\isanewline
+\isacommand{proof}\ intro{\isacharunderscore}classes\isanewline
+\ \ \isacommand{fix}\ x\ y\ z\ ::\ {\isachardoublequote}{\isacharprime}a{\isasymColon}monoid{\isachardoublequote}\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ monoid.assoc{\isacharparenright}\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\ {\isacharless}\ monoid\isanewline
+\isacommand{proof}\ intro{\isacharunderscore}classes\isanewline
+\ \ \isacommand{fix}\ x\ y\ z\ ::\ {\isachardoublequote}{\isacharprime}a{\isasymColon}group{\isachardoublequote}\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ semigroup.assoc{\isacharparenright}\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ group.left{\isacharunderscore}unit{\isacharparenright}\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline
 \isacommand{qed}%
 \begin{isamarkuptext}%
 \medskip The $\isakeyword{instance}$ command sets up an appropriate
@@ -214,10 +214,10 @@
  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}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
+\ \ times{\isacharunderscore}bool{\isacharunderscore}def:\ \ \ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ inverse{\isacharunderscore}bool{\isacharunderscore}def:\ {\isachardoublequote}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequote}\isanewline
+\ \ unit{\isacharunderscore}bool{\isacharunderscore}def:\ \ \ \ {\isachardoublequote}{\isasymunit}\ {\isasymequiv}\ False{\isachardoublequote}%
 \begin{isamarkuptext}%
 \medskip It is important to note that above $\DEFS$ are just
  overloaded meta-level constant definitions, where type classes are
@@ -233,13 +233,13 @@
  :: 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{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes,\isanewline
+\ \ \ \ unfold\ times{\isacharunderscore}bool{\isacharunderscore}def\ inverse{\isacharunderscore}bool{\isacharunderscore}def\ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\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{show}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isasymnoteq}\ z{\isacharparenright}\ =\ {\isacharparenleft}x\ {\isasymnoteq}\ {\isacharparenleft}y\ {\isasymnoteq}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequote}\ \isacommand{by}\ blast\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}False\ {\isasymnoteq}\ x{\isacharparenright}\ =\ x{\isachardoublequote}\ \isacommand{by}\ blast\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ x{\isacharparenright}\ =\ False{\isachardoublequote}\ \isacommand{by}\ blast\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ =\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequote}\ \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}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
+\ \ times{\isacharunderscore}prod{\isacharunderscore}def:\ {\isachardoublequote}p\ {\isasymOtimes}\ q\ {\isasymequiv}\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}{\isachardoublequote}%
 \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{instance}\ {\isacharasterisk}\ ::\ {\isacharparenleft}semigroup,\ semigroup{\isacharparenright}\ semigroup\isanewline
+\isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes,\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline
+\ \ \isacommand{fix}\ p\ q\ r\ ::\ {\isachardoublequote}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequote}\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
+\ \ \ \ {\isachardoublequote}{\isacharparenleft}fst\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}\ {\isasymOtimes}\ fst\ r,\isanewline
+\ \ \ \ \ \ snd\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}\ {\isasymOtimes}\ snd\ r{\isacharparenright}\ =\isanewline
+\ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ {\isacharparenleft}fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r{\isacharparenright},\isanewline
+\ \ \ \ \ \ \ \ snd\ p\ {\isasymOtimes}\ snd\ {\isacharparenleft}fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ add:\ semigroup.assoc{\isacharparenright}\isanewline
 \isacommand{qed}%
 \begin{isamarkuptext}%
 Thus, if we view class instances as ``structures'', then overloaded

--- a/doc-src/AxClass/generated/NatClass.tex	Sun Aug 20 17:45:20 2000 +0200
+++ b/doc-src/AxClass/generated/NatClass.tex	Mon Aug 21 13:47:24 2000 +0200
@@ -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\ ::\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}0{\isachardoublequote}{\isacharparenright}\isanewline
+\ \ Suc\ ::\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
+\ \ rec\ ::\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\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\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\ \ induct:\ \ \ \ \ {\isachardoublequote}P{\isacharparenleft}0{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x.\ P{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}Suc{\isacharparenleft}x{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}n{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ Suc{\isacharunderscore}inject:\ {\isachardoublequote}Suc{\isacharparenleft}m{\isacharparenright}\ =\ Suc{\isacharparenleft}n{\isacharparenright}\ {\isasymLongrightarrow}\ m\ =\ n{\isachardoublequote}\isanewline
+\ \ Suc{\isacharunderscore}neq{\isacharunderscore}0:\ \ {\isachardoublequote}Suc{\isacharparenleft}m{\isacharparenright}\ =\ 0\ {\isasymLongrightarrow}\ R{\isachardoublequote}\isanewline
+\ \ rec{\isacharunderscore}0:\ \ \ \ \ \ {\isachardoublequote}rec{\isacharparenleft}0,\ a,\ f{\isacharparenright}\ =\ a{\isachardoublequote}\isanewline
+\ \ rec{\isacharunderscore}Suc:\ \ \ \ {\isachardoublequote}rec{\isacharparenleft}Suc{\isacharparenleft}m{\isacharparenright},\ a,\ f{\isacharparenright}\ =\ f{\isacharparenleft}m,\ rec{\isacharparenleft}m,\ a,\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}\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\ ::\ {\isachardoublequote}{\isacharprime}a::nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}+{\isachardoublequote}\ 60{\isacharparenright}\isanewline
+\ \ {\isachardoublequote}m\ +\ n\ {\isasymequiv}\ rec{\isacharparenleft}m,\ n,\ {\isasymlambda}x\ y.\ Suc{\isacharparenleft}y{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 This is an abstract version of the plain $Nat$ theory in
  FOL.\footnote{See

--- a/doc-src/AxClass/generated/Product.tex	Sun Aug 20 17:45:20 2000 +0200
+++ b/doc-src/AxClass/generated/Product.tex	Mon Aug 21 13:47:24 2000 +0200
@@ -17,9 +17,9 @@
  syntactic type classes.%
 \end{isamarkuptext}%
 \isacommand{axclass}\isanewline
-\ \ product\ <\ {"}term{"}\isanewline
+\ \ product\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
 \isacommand{consts}\isanewline
-\ \ product\ ::\ {"}'a::product\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOtimes}{"}\ 70)%
+\ \ product\ ::\ {\isachardoublequote}{\isacharprime}a::product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ 70{\isacharparenright}%
 \begin{isamarkuptext}%
 Here class $product$ is defined as subclass of $term$ without any
  additional axioms.  This effects in logical equivalence of $product$
@@ -49,9 +49,9 @@
  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{by}\ intro{\isacharunderscore}classes\isanewline
+\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
+\ \ product{\isacharunderscore}bool{\isacharunderscore}def:\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}%
 \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	Sun Aug 20 17:45:20 2000 +0200
+++ b/doc-src/AxClass/generated/Semigroups.tex	Mon Aug 21 13:47:24 2000 +0200
@@ -15,10 +15,10 @@
  semigroups.%
 \end{isamarkuptext}%
 \isacommand{consts}\isanewline
-\ \ times\ ::\ {"}'a\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOtimes}{"}\ 70)\isanewline
+\ \ times\ ::\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ 70{\isacharparenright}\isanewline
 \isacommand{axclass}\isanewline
-\ \ semigroup\ <\ {"}term{"}\isanewline
-\ \ assoc:\ {"}(x\ {\isasymOtimes}\ y)\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}%
+\ \ semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\ \ assoc:\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}%
 \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\ ::\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOplus}{\isachardoublequote}\ 70{\isacharparenright}\isanewline
 \isacommand{axclass}\isanewline
-\ \ plus\_semigroup\ <\ {"}term{"}\isanewline
-\ \ assoc:\ {"}(x\ {\isasymOplus}\ y)\ {\isasymOplus}\ z\ =\ x\ {\isasymOplus}\ (y\ {\isasymOplus}\ z){"}%
+\ \ plus{\isacharunderscore}semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\ \ assoc:\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOplus}\ y{\isacharparenright}\ {\isasymOplus}\ z\ =\ x\ {\isasymOplus}\ {\isacharparenleft}y\ {\isasymOplus}\ z{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent Even if classes $plus_semigroup$ and $semigroup$ both
  represent semigroups in a sense, they are certainly not quite the

--- a/doc-src/AxClass/generated/isabelle.sty	Sun Aug 20 17:45:20 2000 +0200
+++ b/doc-src/AxClass/generated/isabelle.sty	Mon Aug 21 13:47:24 2000 +0200
@@ -8,26 +8,43 @@
 
 % isabelle environments
 
-\newcommand{\isabellestyle}{\small\tt\slshape}
+\newcommand{\isastyle}{\small\tt\slshape}
+\newcommand{\isastyletext}{\normalsize\rm}
+\newcommand{\isastyletxt}{\rm}
+\newcommand{\isastylecmt}{\rm}
 
 \newdimen\isa@parindent\newdimen\isa@parskip
+
 \newenvironment{isabelle}{%
 \isa@parindent\parindent\parindent0pt%
 \isa@parskip\parskip\parskip0pt%
-\isabellestyle}{}
+\isastyle}{}
 
-\newcommand{\isa}[1]{\emph{\isabellestyle #1}}
-
-\newenvironment{isabellequote}%
-{\begin{quote}\begin{isabelle}\noindent}{\end{isabelle}\end{quote}}
+\newcommand{\isa}[1]{\emph{\isastyle #1}}
 
 \newcommand{\isanewline}{\mbox{}\\\mbox{}}
 
-\chardef\isabraceleft=`\{
-\chardef\isabraceright=`\}
-\chardef\isatilde=`\~
-\chardef\isacircum=`\^
-\chardef\isabackslash=`\\
+\chardef\isacharhash=`\#
+\chardef\isachardollar=`\$
+\chardef\isacharpercent=`\%
+\chardef\isacharampersand=`\&
+\chardef\isacharprime=`\'
+\chardef\isacharparenleft=`\(
+\chardef\isacharparenright=`\)
+\chardef\isacharasterisk=`\*
+\chardef\isacharminus=`\-
+\chardef\isacharless=`\<
+\chardef\isachargreater=`\>
+\chardef\isacharbrackleft=`\[
+\chardef\isachardoublequote=`\"
+\chardef\isacharbackslash=`\\
+\chardef\isacharbrackright=`\]
+\chardef\isacharcircum=`\^
+\chardef\isacharunderscore=`\_
+\chardef\isacharbraceleft=`\{
+\chardef\isacharbar=`\|
+\chardef\isacharbraceright=`\}
+\chardef\isachartilde=`\~
 
 
 % keyword and section markup
@@ -47,6 +64,38 @@
 \newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
 
 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\par\medskip}{\par\smallskip}
-\newenvironment{isamarkuptext}{\normalsize\rm\begin{isapar}}{\end{isapar}}
-\newenvironment{isamarkuptxt}{\rm\begin{isapar}}{\end{isapar}}
-\newcommand{\isamarkupcmt}[1]{{\rm--- #1}}
+\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
+\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
+
+
+% alternative styles -- default is "tt"
+
+\newcommand{\isabellestyle}{}
+\def\isabellestyle#1{\csname isasetup#1\endcsname}
+
+\newcommand{\isasetupit}{%
+\renewcommand{\isastyle}{\small\itshape}%
+\renewcommand{\isastyletext}{\normalsize\rm}%
+\renewcommand{\isastyletxt}{\rm}%
+\renewcommand{\isastylecmt}{\rm}%
+\renewcommand{\isachardollar}{\textsl{\$}}%
+\renewcommand{\isacharampersand}{\textsl{\&}}%
+\renewcommand{\isacharprime}{$'$}%
+\renewcommand{\isacharparenleft}{\emph{$($}}%
+\renewcommand{\isacharparenright}{\emph{$)$}}%
+\renewcommand{\isacharasterisk}{\emph{$*$}}%
+\renewcommand{\isacharminus}{\emph{$-$}}%
+\renewcommand{\isacharless}{\emph{$<$}}%
+\renewcommand{\isachargreater}{\emph{$>$}}%
+\renewcommand{\isachardoublequote}{}%
+\renewcommand{\isacharbrackleft}{\emph{$[$}}%
+\renewcommand{\isacharbrackright}{\emph{$]$}}%
+\renewcommand{\isacharunderscore}{-}%
+\renewcommand{\isacharbraceleft}{\emph{$\{$}}%
+\renewcommand{\isacharbar}{\emph{$\mid$}}%
+\renewcommand{\isacharbraceright}{\emph{$\}$}}%
+}
+
+\newcommand{\isasetupsl}{\isasetupit\renewcommand{\isastyle}{\small\slshape}}
+