diff -r 629f3a92863e -r 0ddd8028f98c doc-src/AxClass/Group/Semigroups.thy
--- a/doc-src/AxClass/Group/Semigroups.thy	Thu Feb 26 10:13:43 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-
-header {* Semigroups *}
-
-theory Semigroups imports Main begin
-
-text {*
-  \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 @{typ
-  'a}.  Class axioms typically contain polymorphic constants that
-  depend on this 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 "\<odot>" 70)
-axclass semigroup \<subseteq> type
-  assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
-
-text {*
-  \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 @{typ 'a} and a fixed
-  \emph{signature}.  Different signatures require different classes.
-  Below, class @{text plus_semigroup} represents semigroups @{text
-  "(\<tau>, \<oplus>\<^sup>\<tau>)"}, while the original @{text semigroup} would
-  correspond to semigroups of the form @{text "(\<tau>, \<odot>\<^sup>\<tau>)"}.
-*}
-
-consts
-  plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<oplus>" 70)
-axclass plus_semigroup \<subseteq> type
-  assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
-
-text {*
-  \noindent Even if classes @{text plus_semigroup} and @{text
-  semigroup} both represent semigroups in a sense, they are certainly
-  not quite the same.
-*}
-
-end