# HG changeset patch
# User wenzelm
# Date 970592123 -7200
# Node ID ba9297b71897da6f0bd69ae8d76938d3ddf28754
# Parent  9fa7d38904881554ad5b3b4a81fc4d90ad96b5c2
major cleanup -- improved typesetting;

diff -r 9fa7d3890488 -r ba9297b71897 doc-src/AxClass/Group/Group.thy
--- a/doc-src/AxClass/Group/Group.thy	Tue Oct 03 18:45:36 2000 +0200
+++ b/doc-src/AxClass/Group/Group.thy	Tue Oct 03 18:55:23 2000 +0200
@@ -4,7 +4,7 @@
 theory Group = Main:
 
 text {*
- \medskip\noindent The meta-type system of Isabelle supports
+ \medskip\noindent The meta-level type system of Isabelle supports
  \emph{intersections} and \emph{inclusions} of type classes. These
  directly correspond to intersections and inclusions of type
  predicates in a purely set theoretic sense. This is sufficient as a
@@ -21,56 +21,53 @@
 *}
 
 consts
-  times :: "'a => 'a => 'a"    (infixl "\<Otimes>" 70)
-  inverse :: "'a => 'a"        ("(_\<inv>)" [1000] 999)
-  one :: 'a                    ("\<unit>")
+  times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
+  inverse :: "'a \<Rightarrow> 'a"    ("(_\<inv>)" [1000] 999)
+  one :: 'a    ("\<unit>")
 
 text {*
- \noindent Next we define class $monoid$ of monoids with operations
- $\TIMES$ and $1$.  Note that multiple class axioms are allowed for
- user convenience --- they simply represent the conjunction of their
- respective universal closures.
+ \noindent Next we define class @{text monoid} of monoids with
+ operations @{text \<odot>} and @{text \<unit>}.  Note that multiple class
+ axioms are allowed for user convenience --- they simply represent the
+ conjunction of their respective universal closures.
 *}
 
-axclass
-  monoid < "term"
-  assoc:      "(x \<Otimes> y) \<Otimes> z = x \<Otimes> (y \<Otimes> z)"
-  left_unit:  "\<unit> \<Otimes> x = x"
-  right_unit: "x \<Otimes> \<unit> = x"
+axclass monoid < "term"
+  assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
+  left_unit: "\<unit> \<odot> x = x"
+  right_unit: "x \<odot> \<unit> = x"
 
 text {*
- \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 the $\TIMES$ operation.
+ \noindent So class @{text monoid} contains exactly those types @{text
+ \<tau>} where @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} and @{text "\<unit> \<Colon> \<tau>"} are
+ specified appropriately, such that @{text \<odot>} is associative and
+ @{text \<unit>} is a left and right unit element for the @{text \<odot>}
+ operation.
 *}
 
 text {*
- \medskip Independently of $monoid$, we now define a linear hierarchy
- of semigroups, general groups and Abelian groups.  Note that the
- names of class axioms are automatically qualified with each class
- name, so we may re-use common names such as $assoc$.
+ \medskip Independently of @{text monoid}, we now define a linear
+ hierarchy of semigroups, general groups and Abelian groups.  Note
+ that the names of class axioms are automatically qualified with each
+ class name, so we may re-use common names such as @{text assoc}.
 *}
 
-axclass
-  semigroup < "term"
-  assoc: "(x \<Otimes> y) \<Otimes> z = x \<Otimes> (y \<Otimes> z)"
+axclass semigroup < "term"
+  assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
 
-axclass
-  group < semigroup
-  left_unit:    "\<unit> \<Otimes> x = x"
-  left_inverse: "x\<inv> \<Otimes> x = \<unit>"
+axclass group < semigroup
+  left_unit: "\<unit> \<odot> x = x"
+  left_inverse: "x\<inv> \<odot> x = \<unit>"
 
-axclass
-  agroup < group
-  commute: "x \<Otimes> y = y \<Otimes> x"
+axclass agroup < group
+  commute: "x \<odot> y = y \<odot> x"
 
 text {*
- \noindent Class $group$ inherits associativity of $\TIMES$ from
- $semigroup$ and adds two further group axioms. Similarly, $agroup$
- is defined as the subset of $group$ such that for all of its elements
- $\tau$, the operation $\TIMES :: \tau \To \tau \To \tau$ is even
- commutative.
+ \noindent Class @{text group} inherits associativity of @{text \<odot>}
+ from @{text semigroup} and adds two further group axioms. Similarly,
+ @{text agroup} is defined as the subset of @{text group} such that
+ for all of its elements @{text \<tau>}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"}
+ is even commutative.
 *}
 
 
@@ -79,13 +76,13 @@
 text {*
  In a sense, axiomatic type classes may be viewed as \emph{abstract
  theories}.  Above class definitions gives rise to abstract axioms
- $assoc$, $left_unit$, $left_inverse$, $commute$, where any of these
- contain a type variable $\alpha :: c$ that is restricted to types of
- the corresponding class $c$.  \emph{Sort constraints} like this
- express a logical precondition for the whole formula.  For example,
- $assoc$ states that for all $\tau$, provided that $\tau ::
- semigroup$, the operation $\TIMES :: \tau \To \tau \To \tau$ is
- associative.
+ @{text assoc}, @{text left_unit}, @{text left_inverse}, @{text
+ commute}, where any of these contain a type variable @{text "'a \<Colon> c"}
+ that is restricted to types of the corresponding class @{text c}.
+ \emph{Sort constraints} like this express a logical precondition for
+ the whole formula.  For example, @{text assoc} states that for all
+ @{text \<tau>}, provided that @{text "\<tau> \<Colon> semigroup"}, the operation
+ @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is associative.
 
  \medskip From a technical point of view, abstract axioms are just
  ordinary Isabelle theorems, which may be used in proofs without
@@ -94,21 +91,21 @@
  well-known laws of general groups.
 *}
 
-theorem group_right_inverse: "x \<Otimes> x\<inv> = (\<unit>\\<Colon>'a\\<Colon>group)"
+theorem group_right_inverse: "x \<odot> x\<inv> = (\<unit>\<Colon>'a\<Colon>group)"
 proof -
-  have "x \<Otimes> x\<inv> = \<unit> \<Otimes> (x \<Otimes> x\<inv>)"
+  have "x \<odot> x\<inv> = \<unit> \<odot> (x \<odot> x\<inv>)"
     by (simp only: group.left_unit)
-  also have "... = \<unit> \<Otimes> x \<Otimes> x\<inv>"
+  also have "... = \<unit> \<odot> x \<odot> x\<inv>"
     by (simp only: semigroup.assoc)
-  also have "... = (x\<inv>)\<inv> \<Otimes> x\<inv> \<Otimes> x \<Otimes> x\<inv>"
+  also have "... = (x\<inv>)\<inv> \<odot> x\<inv> \<odot> x \<odot> x\<inv>"
     by (simp only: group.left_inverse)
-  also have "... = (x\<inv>)\<inv> \<Otimes> (x\<inv> \<Otimes> x) \<Otimes> x\<inv>"
+  also have "... = (x\<inv>)\<inv> \<odot> (x\<inv> \<odot> x) \<odot> x\<inv>"
     by (simp only: semigroup.assoc)
-  also have "... = (x\<inv>)\<inv> \<Otimes> \<unit> \<Otimes> x\<inv>"
+  also have "... = (x\<inv>)\<inv> \<odot> \<unit> \<odot> x\<inv>"
     by (simp only: group.left_inverse)
-  also have "... = (x\<inv>)\<inv> \<Otimes> (\<unit> \<Otimes> x\<inv>)"
+  also have "... = (x\<inv>)\<inv> \<odot> (\<unit> \<odot> x\<inv>)"
     by (simp only: semigroup.assoc)
-  also have "... = (x\<inv>)\<inv> \<Otimes> x\<inv>"
+  also have "... = (x\<inv>)\<inv> \<odot> x\<inv>"
     by (simp only: group.left_unit)
   also have "... = \<unit>"
     by (simp only: group.left_inverse)
@@ -116,18 +113,18 @@
 qed
 
 text {*
- \noindent With $group_right_inverse$ already available,
- $group_right_unit$\label{thm:group-right-unit} is now established
- much easier.
+ \noindent With @{text group_right_inverse} already available, @{text
+ group_right_unit}\label{thm:group-right-unit} is now established much
+ easier.
 *}
 
-theorem group_right_unit: "x \<Otimes> \<unit> = (x\\<Colon>'a\\<Colon>group)"
+theorem group_right_unit: "x \<odot> \<unit> = (x\<Colon>'a\<Colon>group)"
 proof -
-  have "x \<Otimes> \<unit> = x \<Otimes> (x\<inv> \<Otimes> x)"
+  have "x \<odot> \<unit> = x \<odot> (x\<inv> \<odot> x)"
     by (simp only: group.left_inverse)
-  also have "... = x \<Otimes> x\<inv> \<Otimes> x"
+  also have "... = x \<odot> x\<inv> \<odot> x"
     by (simp only: semigroup.assoc)
-  also have "... = \<unit> \<Otimes> x"
+  also have "... = \<unit> \<odot> x"
     by (simp only: group_right_inverse)
   also have "... = x"
     by (simp only: group.left_unit)
@@ -136,24 +133,25 @@
 
 text {*
  \medskip Abstract theorems may be instantiated to only those types
- $\tau$ where the appropriate class membership $\tau :: c$ is known at
- Isabelle's type signature level.  Since we have $agroup \subseteq
- group \subseteq semigroup$ by definition, all theorems of $semigroup$
- and $group$ are automatically inherited by $group$ and $agroup$.
+ @{text \<tau>} where the appropriate class membership @{text "\<tau> \<Colon> c"} is
+ known at Isabelle's type signature level.  Since we have @{text
+ "agroup \<subseteq> group \<subseteq> semigroup"} by definition, all theorems of @{text
+ semigroup} and @{text group} are automatically inherited by @{text
+ group} and @{text agroup}.
 *}
 
 
 subsection {* Abstract instantiation *}
 
 text {*
- From the definition, the $monoid$ and $group$ classes have been
- independent.  Note that for monoids, $right_unit$ had to be included
- as an axiom, but for groups both $right_unit$ and $right_inverse$ are
- derivable from the other axioms.  With $group_right_unit$ derived as
- a theorem of group theory (see page~\pageref{thm:group-right-unit}),
- we may now instantiate $monoid \subseteq semigroup$ and $group
- \subseteq monoid$ properly as follows
- (cf.\ \figref{fig:monoid-group}).
+ From the definition, the @{text monoid} and @{text group} classes
+ have been independent.  Note that for monoids, @{text right_unit} had
+ to be included as an axiom, but for groups both @{text right_unit}
+ and @{text right_inverse} are derivable from the other axioms.  With
+ @{text group_right_unit} derived as a theorem of group theory (see
+ page~\pageref{thm:group-right-unit}), we may now instantiate @{text
+ "monoid \<subseteq> semigroup"} and @{text "group \<subseteq> monoid"} properly as
+ follows (cf.\ \figref{fig:monoid-group}).
 
  \begin{figure}[htbp]
    \begin{center}
@@ -162,20 +160,20 @@
      \begin{picture}(65,90)(0,-10)
        \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
        \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}}
-       \put(15,5){\makebox(0,0){$agroup$}}
-       \put(15,25){\makebox(0,0){$group$}}
-       \put(15,45){\makebox(0,0){$semigroup$}}
-       \put(30,65){\makebox(0,0){$term$}} \put(50,45){\makebox(0,0){$monoid$}}
+       \put(15,5){\makebox(0,0){@{text agroup}}}
+       \put(15,25){\makebox(0,0){@{text group}}}
+       \put(15,45){\makebox(0,0){@{text semigroup}}}
+       \put(30,65){\makebox(0,0){@{text "term"}}} \put(50,45){\makebox(0,0){@{text monoid}}}
      \end{picture}
      \hspace{4em}
      \begin{picture}(30,90)(0,0)
        \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
        \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}}
-       \put(15,5){\makebox(0,0){$agroup$}}
-       \put(15,25){\makebox(0,0){$group$}}
-       \put(15,45){\makebox(0,0){$monoid$}}
-       \put(15,65){\makebox(0,0){$semigroup$}}
-       \put(15,85){\makebox(0,0){$term$}}
+       \put(15,5){\makebox(0,0){@{text agroup}}}
+       \put(15,25){\makebox(0,0){@{text group}}}
+       \put(15,45){\makebox(0,0){@{text monoid}}}
+       \put(15,65){\makebox(0,0){@{text semigroup}}}
+       \put(15,85){\makebox(0,0){@{text term}}}
      \end{picture}
      \caption{Monoids and groups: according to definition, and by proof}
      \label{fig:monoid-group}
@@ -185,30 +183,30 @@
 
 instance monoid < semigroup
 proof intro_classes
-  fix x y z :: "'a\\<Colon>monoid"
-  show "x \<Otimes> y \<Otimes> z = x \<Otimes> (y \<Otimes> z)"
+  fix x y z :: "'a\<Colon>monoid"
+  show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
     by (rule monoid.assoc)
 qed
 
 instance group < monoid
 proof intro_classes
-  fix x y z :: "'a\\<Colon>group"
-  show "x \<Otimes> y \<Otimes> z = x \<Otimes> (y \<Otimes> z)"
+  fix x y z :: "'a\<Colon>group"
+  show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
     by (rule semigroup.assoc)
-  show "\<unit> \<Otimes> x = x"
+  show "\<unit> \<odot> x = x"
     by (rule group.left_unit)
-  show "x \<Otimes> \<unit> = x"
+  show "x \<odot> \<unit> = x"
     by (rule group_right_unit)
 qed
 
 text {*
  \medskip The $\isakeyword{instance}$ command sets up an appropriate
  goal that represents the class inclusion (or type arity, see
- \secref{sec:inst-arity}) to be proven
- (see also \cite{isabelle-isar-ref}).  The $intro_classes$ proof
- method does back-chaining of class membership statements wrt.\ the
- hierarchy of any classes defined in the current theory; the effect is
- to reduce to the initial statement to a number of goals that directly
+ \secref{sec:inst-arity}) to be proven (see also
+ \cite{isabelle-isar-ref}).  The @{text intro_classes} proof method
+ does back-chaining of class membership statements wrt.\ the hierarchy
+ of any classes defined in the current theory; the effect is to reduce
+ to the initial statement to a number of goals that directly
  correspond to any class axioms encountered on the path upwards
  through the class hierarchy.
 *}
@@ -226,15 +224,15 @@
  class membership may be established at the logical level and then
  transferred to Isabelle's type signature level.
 
- \medskip As a typical example, we show that type $bool$ with
- exclusive-or as $\TIMES$ operation, identity as $\isasyminv$, and
- $False$ as $1$ forms an Abelian group.
+ \medskip As a typical example, we show that type @{typ bool} with
+ exclusive-or as @{text \<odot>} operation, identity as @{text \<inv>}, and
+ @{term False} as @{text \<unit>} forms an Abelian group.
 *}
 
 defs (overloaded)
-  times_bool_def:   "x \<Otimes> y \\<equiv> x \\<noteq> (y\\<Colon>bool)"
-  inverse_bool_def: "x\<inv> \\<equiv> x\\<Colon>bool"
-  unit_bool_def:    "\<unit> \\<equiv> False"
+  times_bool_def: "x \<odot> y \<equiv> x \<noteq> (y\<Colon>bool)"
+  inverse_bool_def: "x\<inv> \<equiv> x\<Colon>bool"
+  unit_bool_def: "\<unit> \<equiv> False"
 
 text {*
  \medskip It is important to note that above $\DEFS$ are just
@@ -247,18 +245,18 @@
  best applied in the context of type classes.
 
  \medskip Since we have chosen above $\DEFS$ of the generic group
- operations on type $bool$ appropriately, the class membership $bool
- :: agroup$ may be now derived as follows.
+ operations on type @{typ bool} appropriately, the class membership
+ @{text "bool \<Colon> agroup"} may be now derived as follows.
 *}
 
 instance bool :: agroup
 proof (intro_classes,
     unfold times_bool_def inverse_bool_def unit_bool_def)
   fix x y z
-  show "((x \\<noteq> y) \\<noteq> z) = (x \\<noteq> (y \\<noteq> z))" by blast
-  show "(False \\<noteq> x) = x" by blast
-  show "(x \\<noteq> x) = False" by blast
-  show "(x \\<noteq> y) = (y \\<noteq> x)" by blast
+  show "((x \<noteq> y) \<noteq> z) = (x \<noteq> (y \<noteq> z))" by blast
+  show "(False \<noteq> x) = x" by blast
+  show "(x \<noteq> x) = False" by blast
+  show "(x \<noteq> y) = (y \<noteq> x)" by blast
 qed
 
 text {*
@@ -268,12 +266,13 @@
  care of this new instance automatically.
 
  \medskip We could now also instantiate our group theory classes to
- many other concrete types.  For example, $int :: agroup$ (e.g.\ by
- defining $\TIMES$ as addition, $\isasyminv$ as negation and $1$ as
- zero) or $list :: (term)semigroup$ (e.g.\ if $\TIMES$ is defined as
- list append).  Thus, the characteristic constants $\TIMES$,
- $\isasyminv$, $1$ really become overloaded, i.e.\ have different
- meanings on different types.
+ many other concrete types.  For example, @{text "int \<Colon> agroup"}
+ (e.g.\ by defining @{text \<odot>} as addition, @{text \<inv>} as negation
+ and @{text \<unit>} as zero) or @{text "list \<Colon> (term) semigroup"}
+ (e.g.\ if @{text \<odot>} is defined as list append).  Thus, the
+ characteristic constants @{text \<odot>}, @{text \<inv>}, @{text \<unit>}
+ really become overloaded, i.e.\ have different meanings on different
+ types.
 *}
 
 
@@ -288,27 +287,27 @@
 
  This feature enables us to \emph{lift operations}, say to Cartesian
  products, direct sums or function spaces.  Subsequently we lift
- $\TIMES$ component-wise to binary products $\alpha \times \beta$.
+ @{text \<odot>} component-wise to binary products @{typ "'a \<times> 'b"}.
 *}
 
 defs (overloaded)
-  times_prod_def: "p \<Otimes> q \\<equiv> (fst p \<Otimes> fst q, snd p \<Otimes> snd q)"
+  times_prod_def: "p \<odot> q \<equiv> (fst p \<odot> fst q, snd p \<odot> snd q)"
 
 text {*
- 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.
+ It is very easy to see that associativity of @{text \<odot>} on @{typ 'a}
+ and @{text \<odot>} on @{typ 'b} transfers to @{text \<odot>} on @{typ "'a \<times> 'b"}.
+ Hence the binary type constructor @{text \<odot>} maps semigroups to
+ semigroups.  This may be established formally as follows.
 *}
 
 instance * :: (semigroup, semigroup) semigroup
 proof (intro_classes, unfold times_prod_def)
-  fix p q r :: "'a\\<Colon>semigroup \\<times> 'b\\<Colon>semigroup"
+  fix p q r :: "'a\<Colon>semigroup \<times> 'b\<Colon>semigroup"
   show
-    "(fst (fst p \<Otimes> fst q, snd p \<Otimes> snd q) \<Otimes> fst r,
-      snd (fst p \<Otimes> fst q, snd p \<Otimes> snd q) \<Otimes> snd r) =
-       (fst p \<Otimes> fst (fst q \<Otimes> fst r, snd q \<Otimes> snd r),
-        snd p \<Otimes> snd (fst q \<Otimes> fst r, snd q \<Otimes> snd r))"
+    "(fst (fst p \<odot> fst q, snd p \<odot> snd q) \<odot> fst r,
+      snd (fst p \<odot> fst q, snd p \<odot> snd q) \<odot> snd r) =
+       (fst p \<odot> fst (fst q \<odot> fst r, snd q \<odot> snd r),
+        snd p \<odot> snd (fst q \<odot> fst r, snd q \<odot> snd r))"
     by (simp add: semigroup.assoc)
 qed
 
diff -r 9fa7d3890488 -r ba9297b71897 doc-src/AxClass/Group/Product.thy
--- a/doc-src/AxClass/Group/Product.thy	Tue Oct 03 18:45:36 2000 +0200
+++ b/doc-src/AxClass/Group/Product.thy	Tue Oct 03 18:55:23 2000 +0200
@@ -6,67 +6,70 @@
 text {*
  \medskip\noindent There is still a feature of Isabelle's type system
  left that we have not yet discussed.  When declaring polymorphic
- constants $c :: \sigma$, the type variables occurring in $\sigma$ may
- be constrained by type classes (or even general sorts) in an
+ constants @{text "c \<Colon> \<sigma>"}, the type variables occurring in @{text \<sigma>}
+ may be constrained by type classes (or even general sorts) in an
  arbitrary way.  Note that by default, in Isabelle/HOL the declaration
- $\TIMES :: \alpha \To \alpha \To \alpha$ is actually an abbreviation
- for $\TIMES :: (\alpha::term) \To \alpha \To \alpha$.  Since class
- $term$ is the universal class of HOL, this is not really a constraint
- at all.
+ @{text "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} is actually an abbreviation for
+ @{text "\<odot> \<Colon> 'a\<Colon>term \<Rightarrow> 'a \<Rightarrow> 'a"} Since class @{text "term"} is the
+ universal class of HOL, this is not really a constraint at all.
 
- The $product$ class below provides a less degenerate example of
+ The @{text product} class below provides a less degenerate example of
  syntactic type classes.
 *}
 
 axclass
   product < "term"
 consts
-  product :: "'a::product \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\\<Otimes>" 70)
+  product :: "'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
 
 text {*
- Here class $product$ is defined as subclass of $term$ without any
- additional axioms.  This effects in logical equivalence of $product$
- and $term$, as is reflected by the trivial introduction rule
- generated for this definition.
+ Here class @{text product} is defined as subclass of @{text term}
+ without any additional axioms.  This effects in logical equivalence
+ of @{text product} and @{text term}, as is reflected by the trivial
+ introduction rule generated for this definition.
 
- \medskip So what is the difference of declaring $\TIMES :: (\alpha ::
- product) \To \alpha \To \alpha$ vs.\ declaring $\TIMES :: (\alpha ::
- term) \To \alpha \To \alpha$ anyway?  In this particular case where
- $product \equiv term$, it should be obvious that both declarations
- are the same from the logic's point of view.  It even makes the most
- sense to remove sort constraints from constant declarations, as far
- as the purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}.
+ \medskip So what is the difference of declaring
+ @{text "\<odot> \<Colon> 'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"} vs.\ declaring
+ @{text "\<odot> \<Colon> 'a\<Colon>term \<Rightarrow> 'a \<Rightarrow> 'a"} anyway?  In this particular case
+ where @{text "product \<equiv> term"}, it should be obvious that both
+ declarations are the same from the logic's point of view.  It even
+ makes the most sense to remove sort constraints from constant
+ declarations, as far as the purely logical meaning is concerned
+ \cite{Wenzel:1997:TPHOL}.
 
  On the other hand there are syntactic differences, of course.
- Constants $\TIMES^\tau$ are rejected by the type-checker, unless the
- arity $\tau :: product$ is part of the type signature.  In our
- example, this arity may be always added when required by means of an
- $\isarkeyword{instance}$ with the trivial proof $\BY{intro_classes}$.
+ Constants @{text \<odot>} on some type @{text \<tau>} are rejected by the
+ type-checker, unless the arity @{text "\<tau> \<Colon> product"} is part of the
+ type signature.  In our example, this arity may be always added when
+ required by means of an $\isarkeyword{instance}$ with the trivial
+ proof $\BY{intro_classes}$.
 
  \medskip Thus, we may observe the following discipline of using
  syntactic classes.  Overloaded polymorphic constants have their type
- arguments restricted to an associated (logically trivial) class $c$.
- Only immediately before \emph{specifying} these constants on a
- certain type $\tau$ do we instantiate $\tau :: c$.
+ arguments restricted to an associated (logically trivial) class
+ @{text c}.  Only immediately before \emph{specifying} these constants
+ on a certain type @{text \<tau>} do we instantiate @{text "\<tau> \<Colon> c"}.
 
- This is done for class $product$ and type $bool$ as follows.
+ This is done for class @{text product} and type @{typ bool} as
+ follows.
 *}
 
 instance bool :: product
   by intro_classes
 defs (overloaded)
-  product_bool_def: "x \\<Otimes> y \\<equiv> x \\<and> y"
+  product_bool_def: "x \<odot> y \<equiv> x \<and> y"
 
 text {*
- The definition $prod_bool_def$ becomes syntactically well-formed only
- after the arity $bool :: product$ is made known to the type checker.
+ The definition @{text prod_bool_def} becomes syntactically
+ well-formed only after the arity @{text "bool \<Colon> product"} is made
+ known to the type checker.
 
  \medskip It is very important to see that above $\DEFS$ are not
  directly connected with $\isarkeyword{instance}$ at all!  We were
- just following our convention to specify $\TIMES$ on $bool$ after
- having instantiated $bool :: product$.  Isabelle does not require
- these definitions, which is in contrast to programming languages like
- Haskell \cite{haskell-report}.
+ just following our convention to specify @{text \<odot>} on @{typ bool}
+ after having instantiated @{text "bool \<Colon> product"}.  Isabelle does
+ not require these definitions, which is in contrast to programming
+ languages like Haskell \cite{haskell-report}.
 
  \medskip While Isabelle type classes and those of Haskell are almost
  the same as far as type-checking and type inference are concerned,
@@ -75,9 +78,9 @@
  Therefore, its \texttt{instance} has a \texttt{where} part that tells
  the system what these ``member functions'' should be.
 
- This style of \texttt{instance} won't make much sense in Isabelle's
- meta-logic, because there is no internal notion of ``providing
- operations'' or even ``names of functions''.
+ This style of \texttt{instance} would not make much sense in
+ Isabelle's meta-logic, because there is no internal notion of
+ ``providing operations'' or even ``names of functions''.
 *}
 
 end
\ No newline at end of file
diff -r 9fa7d3890488 -r ba9297b71897 doc-src/AxClass/Group/Semigroups.thy
--- a/doc-src/AxClass/Group/Semigroups.thy	Tue Oct 03 18:45:36 2000 +0200
+++ b/doc-src/AxClass/Group/Semigroups.thy	Tue Oct 03 18:55:23 2000 +0200
@@ -7,49 +7,47 @@
  \medskip\noindent An axiomatic type class is simply a class of types
  that all meet certain properties, which are also called \emph{class
  axioms}. Thus, type classes may be also understood as type predicates
- --- i.e.\ abstractions over a single type argument $\alpha$.  Class
+ --- i.e.\ abstractions over a single type argument @{typ 'a}.  Class
  axioms typically contain polymorphic constants that depend on this
- type $\alpha$.  These \emph{characteristic constants} behave like
- operations associated with the ``carrier'' type $\alpha$.
+ type @{typ 'a}.  These \emph{characteristic constants} behave like
+ operations associated with the ``carrier'' type @{typ 'a}.
 
  We illustrate these basic concepts by the following formulation of
  semigroups.
 *}
 
 consts
-  times :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\<Otimes>" 70)
-axclass
-  semigroup < "term"
-  assoc: "(x \<Otimes> y) \<Otimes> z = x \<Otimes> (y \<Otimes> z)"
+  times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
+axclass semigroup < "term"
+  assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
 
 text {*
- \noindent Above we have first declared a polymorphic constant $\TIMES
- :: \alpha \To \alpha \To \alpha$ and then defined the class
- $semigroup$ of all types $\tau$ such that $\TIMES :: \tau \To \tau
- \To \tau$ is indeed an associative operator.  The $assoc$ axiom
- contains exactly one type variable, which is invisible in the above
- presentation, though.  Also note that free term variables (like $x$,
- $y$, $z$) are allowed for user convenience --- conceptually all of
- these are bound by outermost universal quantifiers.
+ \noindent Above we have first declared a polymorphic constant @{text
+ "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} and then defined the class @{text semigroup} of
+ all types @{text \<tau>} such that @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is indeed an
+ associative operator.  The @{text assoc} axiom contains exactly one
+ type variable, which is invisible in the above presentation, though.
+ Also note that free term variables (like @{term x}, @{term y}, @{term
+ z}) are allowed for user convenience --- conceptually all of these
+ are bound by outermost universal quantifiers.
 
  \medskip In general, type classes may be used to describe
- \emph{structures} with exactly one carrier $\alpha$ and a fixed
+ \emph{structures} with exactly one carrier @{typ 'a} and a fixed
  \emph{signature}.  Different signatures require different classes.
- Below, class $plus_semigroup$ represents semigroups of the form
- $(\tau, \PLUS^\tau)$, while the original $semigroup$ would correspond
- to semigroups $(\tau, \TIMES^\tau)$.
+ Below, class @{text plus_semigroup} represents semigroups of the form
+ @{text "(\<tau>, \<oplus>)"}, while the original @{text semigroup} would
+ correspond to semigroups @{text "(\<tau>, \<odot>)"}.
 *}
 
 consts
-  plus :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "\<Oplus>" 70)
-axclass
-  plus_semigroup < "term"
-  assoc: "(x \<Oplus> y) \<Oplus> z = x \<Oplus> (y \<Oplus> z)"
+  plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<oplus>" 70)
+axclass plus_semigroup < "term"
+  assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
 
 text {*
- \noindent Even if classes $plus_semigroup$ and $semigroup$ both
- represent semigroups in a sense, they are certainly not quite the
- same.
+ \noindent Even if classes @{text plus_semigroup} and @{text
+ semigroup} both represent semigroups in a sense, they are certainly
+ not quite the same.
 *}
 
 end
\ No newline at end of file
diff -r 9fa7d3890488 -r ba9297b71897 doc-src/AxClass/Nat/NatClass.ML
--- a/doc-src/AxClass/Nat/NatClass.ML	Tue Oct 03 18:45:36 2000 +0200
+++ b/doc-src/AxClass/Nat/NatClass.ML	Tue Oct 03 18:55:23 2000 +0200
@@ -34,7 +34,7 @@
 back();
 back();
 
-Goalw [add_def] "0+n = n";
+Goalw [add_def] "\\<zero>+n = n";
 by (rtac rec_0 1);
 qed "add_0";
 
@@ -50,7 +50,7 @@
 by (Asm_simp_tac 1);
 qed "add_assoc";
 
-Goal "m+0 = m";
+Goal "m+\\<zero> = m";
 by (res_inst_tac [("n","m")] induct 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
diff -r 9fa7d3890488 -r ba9297b71897 doc-src/AxClass/Nat/NatClass.thy
--- a/doc-src/AxClass/Nat/NatClass.thy	Tue Oct 03 18:45:36 2000 +0200
+++ b/doc-src/AxClass/Nat/NatClass.thy	Tue Oct 03 18:55:23 2000 +0200
@@ -15,34 +15,33 @@
 *}
 
 consts
-  zero :: 'a    ("0")
-  Suc :: "'a \\<Rightarrow> 'a"
-  rec :: "'a \\<Rightarrow> 'a \\<Rightarrow> ('a \\<Rightarrow> 'a \\<Rightarrow> 'a) \\<Rightarrow> 'a"
+  zero :: 'a    ("\<zero>")
+  Suc :: "'a \<Rightarrow> 'a"
+  rec :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
 
-axclass
-  nat < "term"
-  induct:     "P(0) \\<Longrightarrow> (\\<And>x. P(x) \\<Longrightarrow> P(Suc(x))) \\<Longrightarrow> P(n)"
-  Suc_inject: "Suc(m) = Suc(n) \\<Longrightarrow> m = n"
-  Suc_neq_0:  "Suc(m) = 0 \\<Longrightarrow> R"
-  rec_0:      "rec(0, a, f) = a"
-  rec_Suc:    "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
+axclass nat < "term"
+  induct: "P(\<zero>) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> P(Suc(x))) \<Longrightarrow> P(n)"
+  Suc_inject: "Suc(m) = Suc(n) \<Longrightarrow> m = n"
+  Suc_neq_0: "Suc(m) = \<zero> \<Longrightarrow> R"
+  rec_0: "rec(\<zero>, a, f) = a"
+  rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
 
 constdefs
-  add :: "'a::nat \\<Rightarrow> 'a \\<Rightarrow> 'a"    (infixl "+" 60)
-  "m + n \\<equiv> rec(m, n, \\<lambda>x y. Suc(y))"
+  add :: "'a::nat \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "+" 60)
+  "m + n \<equiv> rec(m, n, \<lambda>x y. Suc(y))"
 
 text {*
- This is an abstract version of the plain $Nat$ theory in
+ This is an abstract version of the plain @{text Nat} theory in
  FOL.\footnote{See
  \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}} Basically,
- we have just replaced all occurrences of type $nat$ by $\alpha$ and
- used the natural number axioms to define class $nat$.  There is only
- a minor snag, that the original recursion operator $rec$ had to be
- made monomorphic.
+ we have just replaced all occurrences of type @{text nat} by @{typ
+ 'a} and used the natural number axioms to define class @{text nat}.
+ There is only a minor snag, that the original recursion operator
+ @{term rec} had to be made monomorphic.
 
- Thus class $nat$ contains exactly those types $\tau$ that are
- isomorphic to ``the'' natural numbers (with signature $0$, $Suc$,
- $rec$).
+ Thus class @{text nat} contains exactly those types @{text \<tau>} that
+ are isomorphic to ``the'' natural numbers (with signature @{term
+ \<zero>}, @{term Suc}, @{term rec}).
 
  \medskip What we have done here can be also viewed as \emph{type
  specification}.  Of course, it still remains open if there is some
diff -r 9fa7d3890488 -r ba9297b71897 doc-src/AxClass/axclass.tex
--- a/doc-src/AxClass/axclass.tex	Tue Oct 03 18:45:36 2000 +0200
+++ b/doc-src/AxClass/axclass.tex	Tue Oct 03 18:55:23 2000 +0200
@@ -1,15 +1,13 @@
 
 \documentclass[12pt,a4paper,fleqn]{report}
-\usepackage{graphicx,../iman,../extra,../isar,../pdfsetup}
+\usepackage{graphicx,../iman,../extra,../isar}
 \usepackage{generated/isabelle,generated/isabellesym}
+\usepackage{../pdfsetup}  % last one!
 
-\newcommand{\TIMES}{\cdot}
-\newcommand{\PLUS}{\oplus}
-\newcommand{\isasymOtimes}{\emph{$\cdot$}}
-\newcommand{\isasymOplus}{\emph{$\oplus$}}
+\isabellestyle{it}
 \newcommand{\isasyminv}{\emph{${}^{-1}$}}
 \newcommand{\isasymunit}{\emph{$1$}}
-
+\newcommand{\isasymzero}{\emph{$0$}}
 
 \newcommand{\secref}[1]{\S\ref{#1}}
 \newcommand{\figref}[1]{figure~\ref{#1}}
diff -r 9fa7d3890488 -r ba9297b71897 doc-src/AxClass/body.tex
--- a/doc-src/AxClass/body.tex	Tue Oct 03 18:45:36 2000 +0200
+++ b/doc-src/AxClass/body.tex	Tue Oct 03 18:55:23 2000 +0200
@@ -44,7 +44,7 @@
 object-logic that directly uses the meta type system, such as Isabelle/HOL
 \cite{isabelle-HOL}.  Subsequently, we present various examples that are all
 formulated within HOL, except the one of \secref{sec:ex-natclass} which is in
-FOL.  See also \url{http://isabelle.in.tum.de/library/HOL/AxClass/} and
+FOL.  See also \url{http://isabelle.in.tum.de/library/HOL/AxClasses/} and
 \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}.
 
 \input{generated/Semigroups}
diff -r 9fa7d3890488 -r ba9297b71897 doc-src/AxClass/generated/Group.tex
--- a/doc-src/AxClass/generated/Group.tex	Tue Oct 03 18:45:36 2000 +0200
+++ b/doc-src/AxClass/generated/Group.tex	Tue Oct 03 18:55:23 2000 +0200
@@ -5,7 +5,7 @@
 \isamarkupheader{Basic group theory}
 \isacommand{theory}\ Group\ {\isacharequal}\ Main{\isacharcolon}%
 \begin{isamarkuptext}%
-\medskip\noindent The meta-type system of Isabelle supports
+\medskip\noindent The meta-level type system of Isabelle supports
  \emph{intersections} and \emph{inclusions} of type classes. These
  directly correspond to intersections and inclusions of type
  predicates in a purely set theoretic sense. This is sufficient as a
@@ -21,51 +21,47 @@
  signature parts of our structures.%
 \end{isamarkuptext}%
 \isacommand{consts}\isanewline
-\ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ {\isacharequal}{\isachargreater}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ \isadigit{7}\isadigit{0}{\isacharparenright}\isanewline
-\ \ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isacharequal}{\isachargreater}\ {\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}{\isasymunit}{\isachardoublequote}{\isacharparenright}%
+\ \ 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
+\ \ inverse\ {\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}{\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
- user convenience --- they simply represent the conjunction of their
- respective universal closures.%
+\noindent Next we define class \isa{monoid} of monoids with
+ operations \isa{{\isasymodot}} and \isa{{\isasymunit}}.  Note that multiple class
+ axioms are allowed for user convenience --- they simply represent the
+ conjunction of their respective universal closures.%
 \end{isamarkuptext}%
-\isacommand{axclass}\isanewline
-\ \ monoid\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
-\ \ assoc{\isacharcolon}\ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ {\isacharequal}\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ left{\isacharunderscore}unit{\isacharcolon}\ \ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
-\ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}%
+\isacommand{axclass}\ monoid\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\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}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
+\ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ 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
- appropriately, such that $\TIMES$ is associative and $1$ is a left
- and right unit element for the $\TIMES$ operation.%
+\noindent So class \isa{monoid} contains exactly those types \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymunit}\ {\isasymColon}\ {\isasymtau}} are
+ specified appropriately, such that \isa{{\isasymodot}} is associative and
+ \isa{{\isasymunit}} is a left and right unit element for the \isa{{\isasymodot}}
+ operation.%
 \end{isamarkuptext}%
 %
 \begin{isamarkuptext}%
-\medskip Independently of $monoid$, we now define a linear hierarchy
- of semigroups, general groups and Abelian groups.  Note that the
- names of class axioms are automatically qualified with each class
- name, so we may re-use common names such as $assoc$.%
+\medskip Independently of \isa{monoid}, we now define a linear
+ hierarchy of semigroups, general groups and Abelian groups.  Note
+ 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}%
-\isacommand{axclass}\isanewline
-\ \ semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
-\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ {\isacharequal}\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{axclass}\ semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
 \isanewline
-\isacommand{axclass}\isanewline
-\ \ group\ {\isacharless}\ semigroup\isanewline
-\ \ left{\isacharunderscore}unit{\isacharcolon}\ \ \ \ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
-\ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymOtimes}\ x\ {\isacharequal}\ {\isasymunit}{\isachardoublequote}\isanewline
+\isacommand{axclass}\ group\ {\isacharless}\ semigroup\isanewline
+\ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
+\ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymodot}\ x\ {\isacharequal}\ {\isasymunit}{\isachardoublequote}\isanewline
 \isanewline
-\isacommand{axclass}\isanewline
-\ \ agroup\ {\isacharless}\ group\isanewline
-\ \ commute{\isacharcolon}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isacharequal}\ y\ {\isasymOtimes}\ x{\isachardoublequote}%
+\isacommand{axclass}\ agroup\ {\isacharless}\ group\isanewline
+\ \ commute{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequote}%
 \begin{isamarkuptext}%
-\noindent Class $group$ inherits associativity of $\TIMES$ from
- $semigroup$ and adds two further group axioms. Similarly, $agroup$
- is defined as the subset of $group$ such that for all of its elements
- $\tau$, the operation $\TIMES :: \tau \To \tau \To \tau$ is even
- commutative.%
+\noindent Class \isa{group} inherits associativity of \isa{{\isasymodot}}
+ from \isa{semigroup} and adds two further group axioms. Similarly,
+ \isa{agroup} is defined as the subset of \isa{group} such that
+ for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}}
+ is even commutative.%
 \end{isamarkuptext}%
 %
 \isamarkupsubsection{Abstract reasoning}
@@ -73,13 +69,12 @@
 \begin{isamarkuptext}%
 In a sense, axiomatic type classes may be viewed as \emph{abstract
  theories}.  Above class definitions gives rise to abstract axioms
- $assoc$, $left_unit$, $left_inverse$, $commute$, where any of these
- contain a type variable $\alpha :: c$ that is restricted to types of
- the corresponding class $c$.  \emph{Sort constraints} like this
- express a logical precondition for the whole formula.  For example,
- $assoc$ states that for all $\tau$, provided that $\tau ::
- semigroup$, the operation $\TIMES :: \tau \To \tau \To \tau$ is
- associative.
+ \isa{assoc}, \isa{left{\isacharunderscore}unit}, \isa{left{\isacharunderscore}inverse}, \isa{commute}, where any of these contain a type variable \isa{{\isacharprime}a\ {\isasymColon}\ c}
+ that is restricted to types of the corresponding class \isa{c}.
+ \emph{Sort constraints} like this express a logical precondition for
+ the whole formula.  For example, \isa{assoc} states that for all
+ \isa{{\isasymtau}}, provided that \isa{{\isasymtau}\ {\isasymColon}\ semigroup}, the operation
+ \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is associative.
 
  \medskip From a technical point of view, abstract axioms are just
  ordinary Isabelle theorems, which may be used in proofs without
@@ -87,38 +82,37 @@
  ``abstract theorems''.  For example, we may now derive the following
  well-known laws of general groups.%
 \end{isamarkuptext}%
-\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymOtimes}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymunit}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymunit}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{proof}\ {\isacharminus}\isanewline
-\ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymOtimes}\ x{\isasyminv}\ {\isacharequal}\ {\isasymunit}\ {\isasymOtimes}\ {\isacharparenleft}x\ {\isasymOtimes}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isacharparenleft}x{\isasyminv}\ {\isasymOtimes}\ x{\isacharparenright}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymunit}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ {\isacharparenleft}{\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymunit}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}{\isachardoublequote}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
 \ \ \isacommand{finally}\ \isacommand{show}\ {\isacharquery}thesis\ \isacommand{{\isachardot}}\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.%
+\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}%
-\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{proof}\ {\isacharminus}\isanewline
-\ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ {\isacharequal}\ x\ {\isasymOtimes}\ {\isacharparenleft}x{\isasyminv}\ {\isasymOtimes}\ x{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x{\isachardoublequote}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
-\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymOtimes}\ x{\isachardoublequote}\isanewline
+\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ x{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline
 \ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
@@ -126,23 +120,20 @@
 \isacommand{qed}%
 \begin{isamarkuptext}%
 \medskip Abstract theorems may be instantiated to only those types
- $\tau$ where the appropriate class membership $\tau :: c$ is known at
- Isabelle's type signature level.  Since we have $agroup \subseteq
- group \subseteq semigroup$ by definition, all theorems of $semigroup$
- and $group$ are automatically inherited by $group$ and $agroup$.%
+ \isa{{\isasymtau}} where the appropriate class membership \isa{{\isasymtau}\ {\isasymColon}\ c} is
+ known at Isabelle's type signature level.  Since we have \isa{agroup\ {\isasymsubseteq}\ group\ {\isasymsubseteq}\ semigroup} by definition, all theorems of \isa{semigroup} and \isa{group} are automatically inherited by \isa{group} and \isa{agroup}.%
 \end{isamarkuptext}%
 %
 \isamarkupsubsection{Abstract instantiation}
 %
 \begin{isamarkuptext}%
-From the definition, the $monoid$ and $group$ classes have been
- independent.  Note that for monoids, $right_unit$ had to be included
- as an axiom, but for groups both $right_unit$ and $right_inverse$ are
- derivable from the other axioms.  With $group_right_unit$ derived as
- a theorem of group theory (see page~\pageref{thm:group-right-unit}),
- we may now instantiate $monoid \subseteq semigroup$ and $group
- \subseteq monoid$ properly as follows
- (cf.\ \figref{fig:monoid-group}).
+From the definition, the \isa{monoid} and \isa{group} classes
+ have been independent.  Note that for monoids, \isa{right{\isacharunderscore}unit} had
+ to be included as an axiom, but for groups both \isa{right{\isacharunderscore}unit}
+ and \isa{right{\isacharunderscore}inverse} are derivable from the other axioms.  With
+ \isa{group{\isacharunderscore}right{\isacharunderscore}unit} derived as a theorem of group theory (see
+ page~\pageref{thm:group-right-unit}), we may now instantiate \isa{monoid\ {\isasymsubseteq}\ semigroup} and \isa{group\ {\isasymsubseteq}\ monoid} properly as
+ follows (cf.\ \figref{fig:monoid-group}).
 
  \begin{figure}[htbp]
    \begin{center}
@@ -151,20 +142,20 @@
      \begin{picture}(65,90)(0,-10)
        \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
        \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}}
-       \put(15,5){\makebox(0,0){$agroup$}}
-       \put(15,25){\makebox(0,0){$group$}}
-       \put(15,45){\makebox(0,0){$semigroup$}}
-       \put(30,65){\makebox(0,0){$term$}} \put(50,45){\makebox(0,0){$monoid$}}
+       \put(15,5){\makebox(0,0){\isa{agroup}}}
+       \put(15,25){\makebox(0,0){\isa{group}}}
+       \put(15,45){\makebox(0,0){\isa{semigroup}}}
+       \put(30,65){\makebox(0,0){\isa{term}}} \put(50,45){\makebox(0,0){\isa{monoid}}}
      \end{picture}
      \hspace{4em}
      \begin{picture}(30,90)(0,0)
        \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
        \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}}
-       \put(15,5){\makebox(0,0){$agroup$}}
-       \put(15,25){\makebox(0,0){$group$}}
-       \put(15,45){\makebox(0,0){$monoid$}}
-       \put(15,65){\makebox(0,0){$semigroup$}}
-       \put(15,85){\makebox(0,0){$term$}}
+       \put(15,5){\makebox(0,0){\isa{agroup}}}
+       \put(15,25){\makebox(0,0){\isa{group}}}
+       \put(15,45){\makebox(0,0){\isa{monoid}}}
+       \put(15,65){\makebox(0,0){\isa{semigroup}}}
+       \put(15,85){\makebox(0,0){\isa{term}}}
      \end{picture}
      \caption{Monoids and groups: according to definition, and by proof}
      \label{fig:monoid-group}
@@ -174,28 +165,28 @@
 \isacommand{instance}\ monoid\ {\isacharless}\ semigroup\isanewline
 \isacommand{proof}\ intro{\isacharunderscore}classes\isanewline
 \ \ \isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}monoid{\isachardoublequote}\isanewline
-\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ {\isacharequal}\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ monoid{\isachardot}assoc{\isacharparenright}\isanewline
 \isacommand{qed}\isanewline
 \isanewline
 \isacommand{instance}\ group\ {\isacharless}\ monoid\isanewline
 \isacommand{proof}\ intro{\isacharunderscore}classes\isanewline
 \ \ \isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}group{\isachardoublequote}\isanewline
-\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ {\isacharequal}\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
-\ \ \isacommand{show}\ {\isachardoublequote}{\isasymunit}\ {\isasymOtimes}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
-\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymOtimes}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}\isanewline
+\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ 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
  goal that represents the class inclusion (or type arity, see
- \secref{sec:inst-arity}) to be proven
- (see also \cite{isabelle-isar-ref}).  The $intro_classes$ proof
- method does back-chaining of class membership statements wrt.\ the
- hierarchy of any classes defined in the current theory; the effect is
- to reduce to the initial statement to a number of goals that directly
+ \secref{sec:inst-arity}) to be proven (see also
+ \cite{isabelle-isar-ref}).  The \isa{intro{\isacharunderscore}classes} proof method
+ does back-chaining of class membership statements wrt.\ the hierarchy
+ of any classes defined in the current theory; the effect is to reduce
+ to the initial statement to a number of goals that directly
  correspond to any class axioms encountered on the path upwards
  through the class hierarchy.%
 \end{isamarkuptext}%
@@ -212,14 +203,14 @@
  class membership may be established at the logical level and then
  transferred to Isabelle's type signature level.
 
- \medskip As a typical example, we show that type $bool$ with
- exclusive-or as $\TIMES$ operation, identity as $\isasyminv$, and
- $False$ as $1$ forms an Abelian group.%
+ \medskip As a typical example, we show that type \isa{bool} with
+ exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and
+ \isa{False} as \isa{{\isasymunit}} forms an Abelian group.%
 \end{isamarkuptext}%
 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-\ \ times{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ \ \ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequote}\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}{\isasymunit}\ {\isasymequiv}\ False{\isachardoublequote}%
+\ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\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
@@ -231,8 +222,8 @@
  best applied in the context of type classes.
 
  \medskip Since we have chosen above $\DEFS$ of the generic group
- operations on type $bool$ appropriately, the class membership $bool
- :: agroup$ may be now derived as follows.%
+ operations on type \isa{bool} appropriately, the class membership
+ \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.%
 \end{isamarkuptext}%
 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline
 \isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\isanewline
@@ -250,12 +241,13 @@
  care of this new instance automatically.
 
  \medskip We could now also instantiate our group theory classes to
- many other concrete types.  For example, $int :: agroup$ (e.g.\ by
- defining $\TIMES$ as addition, $\isasyminv$ as negation and $1$ as
- zero) or $list :: (term)semigroup$ (e.g.\ if $\TIMES$ is defined as
- list append).  Thus, the characteristic constants $\TIMES$,
- $\isasyminv$, $1$ really become overloaded, i.e.\ have different
- meanings on different types.%
+ many other concrete types.  For example, \isa{int\ {\isasymColon}\ agroup}
+ (e.g.\ by defining \isa{{\isasymodot}} as addition, \isa{{\isasyminv}} as negation
+ and \isa{{\isasymunit}} as zero) or \isa{list\ {\isasymColon}\ {\isacharparenleft}term{\isacharparenright}\ semigroup}
+ (e.g.\ if \isa{{\isasymodot}} is defined as list append).  Thus, the
+ characteristic constants \isa{{\isasymodot}}, \isa{{\isasyminv}}, \isa{{\isasymunit}}
+ really become overloaded, i.e.\ have different meanings on different
+ types.%
 \end{isamarkuptext}%
 %
 \isamarkupsubsection{Lifting and Functors}
@@ -269,24 +261,24 @@
 
  This feature enables us to \emph{lift operations}, say to Cartesian
  products, direct sums or function spaces.  Subsequently we lift
- $\TIMES$ component-wise to binary products $\alpha \times \beta$.%
+ \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.%
 \end{isamarkuptext}%
 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-\ \ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}p\ {\isasymOtimes}\ q\ {\isasymequiv}\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}{\isachardoublequote}%
+\ \ 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}%
 \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.%
+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}%
 \isacommand{instance}\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
 \isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline
 \ \ \isacommand{fix}\ p\ q\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequote}\isanewline
 \ \ \isacommand{show}\isanewline
-\ \ \ \ {\isachardoublequote}{\isacharparenleft}fst\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}\ {\isasymOtimes}\ fst\ r{\isacharcomma}\isanewline
-\ \ \ \ \ \ snd\ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymOtimes}\ snd\ q{\isacharparenright}\ {\isasymOtimes}\ snd\ r{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymOtimes}\ fst\ {\isacharparenleft}fst\ q\ {\isasymOtimes}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymOtimes}\ snd\ r{\isacharparenright}{\isacharcomma}\isanewline
-\ \ \ \ \ \ \ \ snd\ p\ {\isasymOtimes}\ snd\ {\isacharparenleft}fst\ q\ {\isasymOtimes}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymOtimes}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \ \ {\isachardoublequote}{\isacharparenleft}fst\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ fst\ r{\isacharcomma}\isanewline
+\ \ \ \ \ \ snd\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ snd\ r{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharcomma}\isanewline
+\ \ \ \ \ \ \ \ snd\ p\ {\isasymodot}\ snd\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
 \isacommand{qed}%
 \begin{isamarkuptext}%
diff -r 9fa7d3890488 -r ba9297b71897 doc-src/AxClass/generated/NatClass.tex
--- a/doc-src/AxClass/generated/NatClass.tex	Tue Oct 03 18:45:36 2000 +0200
+++ b/doc-src/AxClass/generated/NatClass.tex	Tue Oct 03 18:55:23 2000 +0200
@@ -15,33 +15,30 @@
  \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}%
 \end{isamarkuptext}%
 \isacommand{consts}\isanewline
-\ \ zero\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}\isadigit{0}{\isachardoublequote}{\isacharparenright}\isanewline
+\ \ zero\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymzero}{\isachardoublequote}{\isacharparenright}\isanewline
 \ \ Suc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
 \ \ rec\ {\isacharcolon}{\isacharcolon}\ {\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\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
-\ \ induct{\isacharcolon}\ \ \ \ \ {\isachardoublequote}P{\isacharparenleft}\isadigit{0}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ P{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}Suc{\isacharparenleft}x{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}n{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{axclass}\ nat\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\ \ induct{\isacharcolon}\ {\isachardoublequote}P{\isacharparenleft}{\isasymzero}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ P{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}Suc{\isacharparenleft}x{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}n{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ Suc{\isacharunderscore}inject{\isacharcolon}\ {\isachardoublequote}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ Suc{\isacharparenleft}n{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
-\ \ Suc{\isacharunderscore}neq{\isacharunderscore}\isadigit{0}{\isacharcolon}\ \ {\isachardoublequote}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ \isadigit{0}\ {\isasymLongrightarrow}\ R{\isachardoublequote}\isanewline
-\ \ rec{\isacharunderscore}\isadigit{0}{\isacharcolon}\ \ \ \ \ \ {\isachardoublequote}rec{\isacharparenleft}\isadigit{0}{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}\ {\isacharequal}\ a{\isachardoublequote}\isanewline
-\ \ rec{\isacharunderscore}Suc{\isacharcolon}\ \ \ \ {\isachardoublequote}rec{\isacharparenleft}Suc{\isacharparenleft}m{\isacharparenright}{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}m{\isacharcomma}\ rec{\isacharparenleft}m{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ Suc{\isacharunderscore}neq{\isacharunderscore}\isadigit{0}{\isacharcolon}\ {\isachardoublequote}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ {\isasymzero}\ {\isasymLongrightarrow}\ R{\isachardoublequote}\isanewline
+\ \ rec{\isacharunderscore}\isadigit{0}{\isacharcolon}\ {\isachardoublequote}rec{\isacharparenleft}{\isasymzero}{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}\ {\isacharequal}\ a{\isachardoublequote}\isanewline
+\ \ rec{\isacharunderscore}Suc{\isacharcolon}\ {\isachardoublequote}rec{\isacharparenleft}Suc{\isacharparenleft}m{\isacharparenright}{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}m{\isacharcomma}\ rec{\isacharparenleft}m{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
 \isanewline
 \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}%
 \begin{isamarkuptext}%
-This is an abstract version of the plain $Nat$ theory in
+This is an abstract version of the plain \isa{Nat} theory in
  FOL.\footnote{See
  \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}} Basically,
- we have just replaced all occurrences of type $nat$ by $\alpha$ and
- used the natural number axioms to define class $nat$.  There is only
- a minor snag, that the original recursion operator $rec$ had to be
- made monomorphic.
+ we have just replaced all occurrences of type \isa{nat} by \isa{{\isacharprime}a} and used the natural number axioms to define class \isa{nat}.
+ There is only a minor snag, that the original recursion operator
+ \isa{rec} had to be made monomorphic.
 
- Thus class $nat$ contains exactly those types $\tau$ that are
- isomorphic to ``the'' natural numbers (with signature $0$, $Suc$,
- $rec$).
+ Thus class \isa{nat} contains exactly those types \isa{{\isasymtau}} that
+ are isomorphic to ``the'' natural numbers (with signature \isa{{\isasymzero}}, \isa{Suc}, \isa{rec}).
 
  \medskip What we have done here can be also viewed as \emph{type
  specification}.  Of course, it still remains open if there is some
diff -r 9fa7d3890488 -r ba9297b71897 doc-src/AxClass/generated/Product.tex
--- a/doc-src/AxClass/generated/Product.tex	Tue Oct 03 18:45:36 2000 +0200
+++ b/doc-src/AxClass/generated/Product.tex	Tue Oct 03 18:55:23 2000 +0200
@@ -7,63 +7,66 @@
 \begin{isamarkuptext}%
 \medskip\noindent There is still a feature of Isabelle's type system
  left that we have not yet discussed.  When declaring polymorphic
- constants $c :: \sigma$, the type variables occurring in $\sigma$ may
- be constrained by type classes (or even general sorts) in an
+ constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}}
+ may be constrained by type classes (or even general sorts) in an
  arbitrary way.  Note that by default, in Isabelle/HOL the declaration
- $\TIMES :: \alpha \To \alpha \To \alpha$ is actually an abbreviation
- for $\TIMES :: (\alpha::term) \To \alpha \To \alpha$.  Since class
- $term$ is the universal class of HOL, this is not really a constraint
- at all.
+ \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} is actually an abbreviation for
+ \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}term\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} Since class \isa{term} is the
+ universal class of HOL, this is not really a constraint at all.
 
- The $product$ class below provides a less degenerate example of
+ The \isa{product} class below provides a less degenerate example of
  syntactic type classes.%
 \end{isamarkuptext}%
 \isacommand{axclass}\isanewline
 \ \ product\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
 \isacommand{consts}\isanewline
-\ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isacharcolon}{\isacharcolon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ \isadigit{7}\isadigit{0}{\isacharparenright}%
+\ \ 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}%
 \begin{isamarkuptext}%
-Here class $product$ is defined as subclass of $term$ without any
- additional axioms.  This effects in logical equivalence of $product$
- and $term$, as is reflected by the trivial introduction rule
- generated for this definition.
+Here class \isa{product} is defined as subclass of \isa{term}
+ without any additional axioms.  This effects in logical equivalence
+ of \isa{product} and \isa{term}, as is reflected by the trivial
+ introduction rule generated for this definition.
 
- \medskip So what is the difference of declaring $\TIMES :: (\alpha ::
- product) \To \alpha \To \alpha$ vs.\ declaring $\TIMES :: (\alpha ::
- term) \To \alpha \To \alpha$ anyway?  In this particular case where
- $product \equiv term$, it should be obvious that both declarations
- are the same from the logic's point of view.  It even makes the most
- sense to remove sort constraints from constant declarations, as far
- as the purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}.
+ \medskip So what is the difference of declaring
+ \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} vs.\ declaring
+ \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}term\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} anyway?  In this particular case
+ where \isa{product\ {\isasymequiv}\ term}, it should be obvious that both
+ declarations are the same from the logic's point of view.  It even
+ makes the most sense to remove sort constraints from constant
+ declarations, as far as the purely logical meaning is concerned
+ \cite{Wenzel:1997:TPHOL}.
 
  On the other hand there are syntactic differences, of course.
- Constants $\TIMES^\tau$ are rejected by the type-checker, unless the
- arity $\tau :: product$ is part of the type signature.  In our
- example, this arity may be always added when required by means of an
- $\isarkeyword{instance}$ with the trivial proof $\BY{intro_classes}$.
+ Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the
+ type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the
+ type signature.  In our example, this arity may be always added when
+ required by means of an $\isarkeyword{instance}$ with the trivial
+ proof $\BY{intro_classes}$.
 
  \medskip Thus, we may observe the following discipline of using
  syntactic classes.  Overloaded polymorphic constants have their type
- arguments restricted to an associated (logically trivial) class $c$.
- Only immediately before \emph{specifying} these constants on a
- certain type $\tau$ do we instantiate $\tau :: c$.
+ arguments restricted to an associated (logically trivial) class
+ \isa{c}.  Only immediately before \emph{specifying} these constants
+ on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}.
 
- This is done for class $product$ and type $bool$ as follows.%
+ This is done for class \isa{product} and type \isa{bool} as
+ follows.%
 \end{isamarkuptext}%
 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product\isanewline
 \ \ \isacommand{by}\ intro{\isacharunderscore}classes\isanewline
 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-\ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}%
+\ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ 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.
+The definition \isa{prod{\isacharunderscore}bool{\isacharunderscore}def} becomes syntactically
+ well-formed only after the arity \isa{bool\ {\isasymColon}\ product} is made
+ known to the type checker.
 
  \medskip It is very important to see that above $\DEFS$ are not
  directly connected with $\isarkeyword{instance}$ at all!  We were
- just following our convention to specify $\TIMES$ on $bool$ after
- having instantiated $bool :: product$.  Isabelle does not require
- these definitions, which is in contrast to programming languages like
- Haskell \cite{haskell-report}.
+ just following our convention to specify \isa{{\isasymodot}} on \isa{bool}
+ after having instantiated \isa{bool\ {\isasymColon}\ product}.  Isabelle does
+ not require these definitions, which is in contrast to programming
+ languages like Haskell \cite{haskell-report}.
 
  \medskip While Isabelle type classes and those of Haskell are almost
  the same as far as type-checking and type inference are concerned,
@@ -72,9 +75,9 @@
  Therefore, its \texttt{instance} has a \texttt{where} part that tells
  the system what these ``member functions'' should be.
 
- This style of \texttt{instance} won't make much sense in Isabelle's
- meta-logic, because there is no internal notion of ``providing
- operations'' or even ``names of functions''.%
+ This style of \texttt{instance} would not make much sense in
+ Isabelle's meta-logic, because there is no internal notion of
+ ``providing operations'' or even ``names of functions''.%
 \end{isamarkuptext}%
 \isacommand{end}\end{isabellebody}%
 %%% Local Variables:
diff -r 9fa7d3890488 -r ba9297b71897 doc-src/AxClass/generated/Semigroups.tex
--- a/doc-src/AxClass/generated/Semigroups.tex	Tue Oct 03 18:45:36 2000 +0200
+++ b/doc-src/AxClass/generated/Semigroups.tex	Tue Oct 03 18:55:23 2000 +0200
@@ -8,45 +8,40 @@
 \medskip\noindent An axiomatic type class is simply a class of types
  that all meet certain properties, which are also called \emph{class
  axioms}. Thus, type classes may be also understood as type predicates
- --- i.e.\ abstractions over a single type argument $\alpha$.  Class
+ --- i.e.\ abstractions over a single type argument \isa{{\isacharprime}a}.  Class
  axioms typically contain polymorphic constants that depend on this
- type $\alpha$.  These \emph{characteristic constants} behave like
- operations associated with the ``carrier'' type $\alpha$.
+ type \isa{{\isacharprime}a}.  These \emph{characteristic constants} behave like
+ operations associated with the ``carrier'' type \isa{{\isacharprime}a}.
 
  We illustrate these basic concepts by the following formulation of
  semigroups.%
 \end{isamarkuptext}%
 \isacommand{consts}\isanewline
-\ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ \isadigit{7}\isadigit{0}{\isacharparenright}\isanewline
-\isacommand{axclass}\isanewline
-\ \ semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
-\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOtimes}\ y{\isacharparenright}\ {\isasymOtimes}\ z\ {\isacharequal}\ x\ {\isasymOtimes}\ {\isacharparenleft}y\ {\isasymOtimes}\ z{\isacharparenright}{\isachardoublequote}%
+\ \ 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
+\isacommand{axclass}\ semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ 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
- $semigroup$ of all types $\tau$ such that $\TIMES :: \tau \To \tau
- \To \tau$ is indeed an associative operator.  The $assoc$ axiom
- contains exactly one type variable, which is invisible in the above
- presentation, though.  Also note that free term variables (like $x$,
- $y$, $z$) are allowed for user convenience --- conceptually all of
- these are bound by outermost universal quantifiers.
+\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
+ all types \isa{{\isasymtau}} such that \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is indeed an
+ associative operator.  The \isa{assoc} axiom contains exactly one
+ type variable, which is invisible in the above presentation, though.
+ Also note that free term variables (like \isa{x}, \isa{y}, \isa{z}) are allowed for user convenience --- conceptually all of these
+ are bound by outermost universal quantifiers.
 
  \medskip In general, type classes may be used to describe
- \emph{structures} with exactly one carrier $\alpha$ and a fixed
+ \emph{structures} with exactly one carrier \isa{{\isacharprime}a} and a fixed
  \emph{signature}.  Different signatures require different classes.
- Below, class $plus_semigroup$ represents semigroups of the form
- $(\tau, \PLUS^\tau)$, while the original $semigroup$ would correspond
- to semigroups $(\tau, \TIMES^\tau)$.%
+ Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups of the form
+ \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}{\isacharparenright}}, while the original \isa{semigroup} would
+ correspond to semigroups \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}{\isacharparenright}}.%
 \end{isamarkuptext}%
 \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
-\isacommand{axclass}\isanewline
-\ \ plus{\isacharunderscore}semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
-\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymOplus}\ y{\isacharparenright}\ {\isasymOplus}\ z\ {\isacharequal}\ x\ {\isasymOplus}\ {\isacharparenleft}y\ {\isasymOplus}\ z{\isacharparenright}{\isachardoublequote}%
+\ \ 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
+\isacommand{axclass}\ plus{\isacharunderscore}semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ 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
- same.%
+\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}%
 \isacommand{end}\end{isabellebody}%
 %%% Local Variables: