# HG changeset patch
# User wenzelm
# Date 1007229152 -3600
# Node ID de0f4a63baa58dce50c9a2073cd024d46ea2c06e
# Parent  7c6a970f0808ed98ed3edfb6f31e48a34050984a
renamed class "term" to "type" (actually "HOL.type");

diff -r 7c6a970f0808 -r de0f4a63baa5 doc-src/AxClass/Group/Group.thy
--- a/doc-src/AxClass/Group/Group.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/AxClass/Group/Group.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -4,20 +4,20 @@
 theory Group = Main:
 
 text {*
- \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
- means to describe simple hierarchies of structures.  As an
- illustration, we use the well-known example of semigroups, monoids,
- general groups and Abelian groups.
+  \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
+  means to describe simple hierarchies of structures.  As an
+  illustration, we use the well-known example of semigroups, monoids,
+  general groups and Abelian groups.
 *}
 
 subsection {* Monoids and Groups *}
 
 text {*
- First we declare some polymorphic constants required later for the
- signature parts of our structures.
+  First we declare some polymorphic constants required later for the
+  signature parts of our structures.
 *}
 
 consts
@@ -26,33 +26,33 @@
   one :: 'a    ("\<unit>")
 
 text {*
- \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.
+  \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 \<subseteq> "term"
+axclass monoid \<subseteq> type
   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 @{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.
+  \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 @{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}.
+  \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 \<subseteq> "term"
+axclass semigroup \<subseteq> type
   assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
 
 axclass group \<subseteq> semigroup
@@ -63,32 +63,32 @@
   commute: "x \<odot> y = y \<odot> x"
 
 text {*
- \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.
+  \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.
 *}
 
 
 subsection {* Abstract reasoning *}
 
 text {*
- In a sense, axiomatic type classes may be viewed as \emph{abstract
- theories}.  Above class definitions gives rise to abstract axioms
- @{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.
+  In a sense, axiomatic type classes may be viewed as \emph{abstract
+  theories}.  Above class definitions gives rise to abstract axioms
+  @{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
- special treatment.  Such ``abstract proofs'' usually yield new
- ``abstract theorems''.  For example, we may now derive the following
- well-known laws of general groups.
+  \medskip From a technical point of view, abstract axioms are just
+  ordinary Isabelle theorems, which may be used in proofs without
+  special treatment.  Such ``abstract proofs'' usually yield new
+  ``abstract theorems''.  For example, we may now derive the following
+  well-known laws of general groups.
 *}
 
 theorem group_right_inverse: "x \<odot> x\<inv> = (\<unit>\<Colon>'a\<Colon>group)"
@@ -113,9 +113,9 @@
 qed
 
 text {*
- \noindent With @{text group_right_inverse} already available, @{text
- 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 \<odot> \<unit> = (x\<Colon>'a\<Colon>group)"
@@ -132,26 +132,26 @@
 qed
 
 text {*
- \medskip Abstract theorems may be instantiated to only those types
- @{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}.
+  \medskip Abstract theorems may be instantiated to only those types
+  @{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 @{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}).
+  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}
@@ -163,7 +163,7 @@
        \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}}}
+       \put(30,65){\makebox(0,0){@{text type}}} \put(50,45){\makebox(0,0){@{text monoid}}}
      \end{picture}
      \hspace{4em}
      \begin{picture}(30,90)(0,0)
@@ -173,7 +173,7 @@
        \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}}}
+       \put(15,85){\makebox(0,0){@{text type}}}
      \end{picture}
      \caption{Monoids and groups: according to definition, and by proof}
      \label{fig:monoid-group}
@@ -200,34 +200,34 @@
 qed
 
 text {*
- \medskip The $\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 initial proof step causes
- 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.
+  \medskip The $\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 initial proof step causes
+  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.
 *}
 
 
 subsection {* Concrete instantiation \label{sec:inst-arity} *}
 
 text {*
- So far we have covered the case of the form $\INSTANCE$~@{text
- "c\<^sub>1 \<subseteq> c\<^sub>2"}, namely \emph{abstract instantiation} ---
- $c@1$ is more special than @{text "c\<^sub>1"} and thus an instance
- of @{text "c\<^sub>2"}.  Even more interesting for practical
- applications are \emph{concrete instantiations} of axiomatic type
- classes.  That is, certain simple schemes @{text "(\<alpha>\<^sub>1, \<dots>,
- \<alpha>\<^sub>n) t \<Colon> c"} of class membership may be established at the
- logical level and then transferred to Isabelle's type signature
- level.
+  So far we have covered the case of the form $\INSTANCE$~@{text
+  "c\<^sub>1 \<subseteq> c\<^sub>2"}, namely \emph{abstract instantiation} ---
+  $c@1$ is more special than @{text "c\<^sub>1"} and thus an instance
+  of @{text "c\<^sub>2"}.  Even more interesting for practical
+  applications are \emph{concrete instantiations} of axiomatic type
+  classes.  That is, certain simple schemes @{text "(\<alpha>\<^sub>1, \<dots>,
+  \<alpha>\<^sub>n) t \<Colon> c"} of 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 @{typ bool} with
- exclusive-or as @{text \<odot>} operation, identity as @{text \<inv>}, and
- @{term False} as @{text \<unit>} 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)
@@ -236,18 +236,18 @@
   unit_bool_def: "\<unit> \<equiv> False"
 
 text {*
- \medskip It is important to note that above $\DEFS$ are just
- overloaded meta-level constant definitions, where type classes are
- not yet involved at all.  This form of constant definition with
- overloading (and optional recursion over the syntactic structure of
- simple types) are admissible as definitional extensions of plain HOL
- \cite{Wenzel:1997:TPHOL}.  The Haskell-style type system is not
- required for overloading.  Nevertheless, overloaded definitions are
- best applied in the context of type classes.
+  \medskip It is important to note that above $\DEFS$ are just
+  overloaded meta-level constant definitions, where type classes are
+  not yet involved at all.  This form of constant definition with
+  overloading (and optional recursion over the syntactic structure of
+  simple types) are admissible as definitional extensions of plain HOL
+  \cite{Wenzel:1997:TPHOL}.  The Haskell-style type system is not
+  required for overloading.  Nevertheless, overloaded definitions are
+  best applied in the context of type classes.
 
- \medskip Since we have chosen above $\DEFS$ of the generic group
- operations on type @{typ bool} appropriately, the class membership
- @{text "bool \<Colon> agroup"} may be now derived as follows.
+  \medskip Since we have chosen above $\DEFS$ of the generic group
+  operations on type @{typ bool} appropriately, the class membership
+  @{text "bool \<Colon> agroup"} may be now derived as follows.
 *}
 
 instance bool :: agroup
@@ -261,44 +261,44 @@
 qed
 
 text {*
- The result of an $\INSTANCE$ statement is both expressed as a theorem
- of Isabelle's meta-logic, and as a type arity of the type signature.
- The latter enables type-inference system to take care of this new
- instance automatically.
+  The result of an $\INSTANCE$ statement is both expressed as a
+  theorem of Isabelle's meta-logic, and as a type arity of the type
+  signature.  The latter enables type-inference system to take care of
+  this new instance automatically.
 
- \medskip We could now also instantiate our group theory classes to
- 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.
+  \medskip We could now also instantiate our group theory classes to
+  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> (type) 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.
 *}
 
 
 subsection {* Lifting and Functors *}
 
 text {*
- As already mentioned above, overloading in the simply-typed HOL
- systems may include recursion over the syntactic structure of types.
- That is, definitional equations @{text "c\<^sup>\<tau> \<equiv> t"} may also
- contain constants of name @{text c} on the right-hand side --- if
- these have types that are structurally simpler than @{text \<tau>}.
+  As already mentioned above, overloading in the simply-typed HOL
+  systems may include recursion over the syntactic structure of types.
+  That is, definitional equations @{text "c\<^sup>\<tau> \<equiv> t"} may also
+  contain constants of name @{text c} on the right-hand side --- if
+  these have types that are structurally simpler than @{text \<tau>}.
 
- This feature enables us to \emph{lift operations}, say to Cartesian
- products, direct sums or function spaces.  Subsequently we lift
- @{text \<odot>} component-wise to binary products @{typ "'a \<times> 'b"}.
+  This feature enables us to \emph{lift operations}, say to Cartesian
+  products, direct sums or function spaces.  Subsequently we lift
+  @{text \<odot>} component-wise to binary products @{typ "'a \<times> 'b"}.
 *}
 
 defs (overloaded)
   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 @{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.
+  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
@@ -313,10 +313,10 @@
 qed
 
 text {*
- Thus, if we view class instances as ``structures'', then overloaded
- constant definitions with recursion over types indirectly provide
- some kind of ``functors'' --- i.e.\ mappings between abstract
- theories.
+  Thus, if we view class instances as ``structures'', then overloaded
+  constant definitions with recursion over types indirectly provide
+  some kind of ``functors'' --- i.e.\ mappings between abstract
+  theories.
 *}
 
-end
\ No newline at end of file
+end
diff -r 7c6a970f0808 -r de0f4a63baa5 doc-src/AxClass/Group/Product.thy
--- a/doc-src/AxClass/Group/Product.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/AxClass/Group/Product.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -4,52 +4,53 @@
 theory Product = Main:
 
 text {*
- \medskip\noindent There is still a feature of Isabelle's type system
- left that we have not yet discussed.  When declaring polymorphic
- 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
- @{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.
+  \medskip\noindent There is still a feature of Isabelle's type system
+  left that we have not yet discussed.  When declaring polymorphic
+  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 @{text "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} is actually an abbreviation
+  for @{text "\<odot> \<Colon> 'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> 'a"} Since class @{text type} is the
+  universal class of HOL, this is not really a constraint at all.
 
  The @{text product} class below provides a less degenerate example of
  syntactic type classes.
 *}
 
 axclass
-  product \<subseteq> "term"
+  product \<subseteq> type
 consts
   product :: "'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
 
 text {*
- 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.
+  Here class @{text product} is defined as subclass of @{text type}
+  without any additional axioms.  This effects in logical equivalence
+  of @{text product} and @{text type}, as is reflected by the trivial
+  introduction rule generated for this definition.
 
- \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}.
+  \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>type \<Rightarrow> 'a \<Rightarrow>
+  'a"} anyway?  In this particular case where @{text "product \<equiv>
+  type"}, 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 @{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 $\INSTANCE$ with the default proof $\DDOT$.
+  On the other hand there are syntactic differences, of course.
+  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 $\INSTANCE$ with the default proof $\DDOT$.
 
- \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
- @{text c}.  Only immediately before \emph{specifying} these constants
- on a certain type @{text \<tau>} do we instantiate @{text "\<tau> \<Colon> c"}.
+  \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
+  @{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 @{text product} and type @{typ bool} as
- follows.
+  This is done for class @{text product} and type @{typ bool} as
+  follows.
 *}
 
 instance bool :: product ..
@@ -80,4 +81,4 @@
  ``providing operations'' or even ``names of functions''.
 *}
 
-end
\ No newline at end of file
+end
diff -r 7c6a970f0808 -r de0f4a63baa5 doc-src/AxClass/Group/Semigroups.thy
--- a/doc-src/AxClass/Group/Semigroups.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/AxClass/Group/Semigroups.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -4,50 +4,51 @@
 theory Semigroups = Main:
 
 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}.
+  \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.
+  We illustrate these basic concepts by the following formulation of
+  semigroups.
 *}
 
 consts
   times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
-axclass semigroup \<subseteq> "term"
+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.
+  \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>)"}.
+  \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> "term"
+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.
+  \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
+end
diff -r 7c6a970f0808 -r de0f4a63baa5 doc-src/AxClass/generated/Group.tex
--- a/doc-src/AxClass/generated/Group.tex	Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/AxClass/generated/Group.tex	Sat Dec 01 18:52:32 2001 +0100
@@ -9,12 +9,12 @@
 %
 \begin{isamarkuptext}%
 \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
- means to describe simple hierarchies of structures.  As an
- illustration, we use the well-known example of semigroups, monoids,
- general groups and Abelian groups.%
+  \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
+  means to describe simple hierarchies of structures.  As an
+  illustration, we use the well-known example of semigroups, monoids,
+  general groups and Abelian groups.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -24,7 +24,7 @@
 %
 \begin{isamarkuptext}%
 First we declare some polymorphic constants required later for the
- signature parts of our structures.%
+  signature parts of our structures.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{consts}\isanewline
@@ -34,32 +34,33 @@
 %
 \begin{isamarkuptext}%
 \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.%
+  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}%
 \isamarkuptrue%
-\isacommand{axclass}\ monoid\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\isacommand{axclass}\ monoid\ {\isasymsubseteq}\ type\isanewline
 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
 \ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
-\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.%
+\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}%
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \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}.%
+  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}%
 \isamarkuptrue%
-\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ type\isanewline
 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
 \isanewline
 \isamarkupfalse%
@@ -73,9 +74,9 @@
 %
 \begin{isamarkuptext}%
 \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.%
+  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}%
 \isamarkuptrue%
 %
@@ -85,19 +86,16 @@
 %
 \begin{isamarkuptext}%
 In a sense, axiomatic type classes may be viewed as \emph{abstract
- theories}.  Above class definitions gives rise to abstract axioms
- \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.
+  theories}.  Above class definitions gives rise to abstract axioms
+  \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
- special treatment.  Such ``abstract proofs'' usually yield new
- ``abstract theorems''.  For example, we may now derive the following
- well-known laws of general groups.%
+  \medskip From a technical point of view, abstract axioms are just
+  ordinary Isabelle theorems, which may be used in proofs without
+  special treatment.  Such ``abstract proofs'' usually yield new
+  ``abstract theorems''.  For example, we may now derive the following
+  well-known laws of general groups.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymunit}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
@@ -150,8 +148,8 @@
 \isacommand{qed}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
-\noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established much
- easier.%
+\noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established
+  much easier.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
@@ -185,8 +183,8 @@
 %
 \begin{isamarkuptext}%
 \medskip Abstract theorems may be instantiated to only those types
- \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}.%
+  \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}%
 \isamarkuptrue%
 %
@@ -196,12 +194,11 @@
 %
 \begin{isamarkuptext}%
 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}).
+  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}
@@ -213,7 +210,7 @@
        \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}}}
+       \put(30,65){\makebox(0,0){\isa{type}}} \put(50,45){\makebox(0,0){\isa{monoid}}}
      \end{picture}
      \hspace{4em}
      \begin{picture}(30,90)(0,0)
@@ -223,7 +220,7 @@
        \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}}}
+       \put(15,85){\makebox(0,0){\isa{type}}}
      \end{picture}
      \caption{Monoids and groups: according to definition, and by proof}
      \label{fig:monoid-group}
@@ -266,14 +263,14 @@
 %
 \begin{isamarkuptext}%
 \medskip The $\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 initial proof step causes
- 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.%
+  represents the class inclusion (or type arity, see
+  \secref{sec:inst-arity}) to be proven (see also
+  \cite{isabelle-isar-ref}).  The initial proof step causes
+  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}%
 \isamarkuptrue%
 %
@@ -283,16 +280,16 @@
 %
 \begin{isamarkuptext}%
 So far we have covered the case of the form $\INSTANCE$~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}}, namely \emph{abstract instantiation} ---
- $c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance
- of \isa{c\isactrlsub {\isadigit{2}}}.  Even more interesting for practical
- applications are \emph{concrete instantiations} of axiomatic type
- classes.  That is, certain simple schemes \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isasymColon}\ c} of class membership may be established at the
- logical level and then transferred to Isabelle's type signature
- level.
+  $c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance
+  of \isa{c\isactrlsub {\isadigit{2}}}.  Even more interesting for practical
+  applications are \emph{concrete instantiations} of axiomatic type
+  classes.  That is, certain simple schemes \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isasymColon}\ c} of 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 \isa{bool} with
- exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and
- \isa{False} as \isa{{\isasymunit}} 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}%
 \isamarkuptrue%
 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
@@ -302,17 +299,17 @@
 %
 \begin{isamarkuptext}%
 \medskip It is important to note that above $\DEFS$ are just
- overloaded meta-level constant definitions, where type classes are
- not yet involved at all.  This form of constant definition with
- overloading (and optional recursion over the syntactic structure of
- simple types) are admissible as definitional extensions of plain HOL
- \cite{Wenzel:1997:TPHOL}.  The Haskell-style type system is not
- required for overloading.  Nevertheless, overloaded definitions are
- best applied in the context of type classes.
+  overloaded meta-level constant definitions, where type classes are
+  not yet involved at all.  This form of constant definition with
+  overloading (and optional recursion over the syntactic structure of
+  simple types) are admissible as definitional extensions of plain HOL
+  \cite{Wenzel:1997:TPHOL}.  The Haskell-style type system is not
+  required for overloading.  Nevertheless, overloaded definitions are
+  best applied in the context of type classes.
 
- \medskip Since we have chosen above $\DEFS$ of the generic group
- operations on type \isa{bool} appropriately, the class membership
- \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.%
+  \medskip Since we have chosen above $\DEFS$ of the generic group
+  operations on type \isa{bool} appropriately, the class membership
+  \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline
@@ -337,19 +334,19 @@
 \isacommand{qed}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
-The result of an $\INSTANCE$ statement is both expressed as a theorem
- of Isabelle's meta-logic, and as a type arity of the type signature.
- The latter enables type-inference system to take care of this new
- instance automatically.
+The result of an $\INSTANCE$ statement is both expressed as a
+  theorem of Isabelle's meta-logic, and as a type arity of the type
+  signature.  The latter enables type-inference system to take care of
+  this new instance automatically.
 
- \medskip We could now also instantiate our group theory classes to
- 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.%
+  \medskip We could now also instantiate our group theory classes to
+  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}type{\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}%
 \isamarkuptrue%
 %
@@ -359,14 +356,14 @@
 %
 \begin{isamarkuptext}%
 As already mentioned above, overloading in the simply-typed HOL
- systems may include recursion over the syntactic structure of types.
- That is, definitional equations \isa{c\isactrlsup {\isasymtau}\ {\isasymequiv}\ t} may also
- contain constants of name \isa{c} on the right-hand side --- if
- these have types that are structurally simpler than \isa{{\isasymtau}}.
+  systems may include recursion over the syntactic structure of types.
+  That is, definitional equations \isa{c\isactrlsup {\isasymtau}\ {\isasymequiv}\ t} may also
+  contain constants of name \isa{c} on the right-hand side --- if
+  these have types that are structurally simpler than \isa{{\isasymtau}}.
 
- This feature enables us to \emph{lift operations}, say to Cartesian
- products, direct sums or function spaces.  Subsequently we lift
- \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.%
+  This feature enables us to \emph{lift operations}, say to Cartesian
+  products, direct sums or function spaces.  Subsequently we lift
+  \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
@@ -374,8 +371,8 @@
 %
 \begin{isamarkuptext}%
 It is very easy to see that associativity of \isa{{\isasymodot}} on \isa{{\isacharprime}a}
- and \isa{{\isasymodot}} on \isa{{\isacharprime}b} transfers to \isa{{\isasymodot}} on \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.  Hence the binary type constructor \isa{{\isasymodot}} maps semigroups to
- semigroups.  This may be established formally as follows.%
+  and \isa{{\isasymodot}} on \isa{{\isacharprime}b} transfers to \isa{{\isasymodot}} on \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.  Hence the binary type constructor \isa{{\isasymodot}} maps semigroups
+  to semigroups.  This may be established formally as follows.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{instance}\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
@@ -396,12 +393,13 @@
 %
 \begin{isamarkuptext}%
 Thus, if we view class instances as ``structures'', then overloaded
- constant definitions with recursion over types indirectly provide
- some kind of ``functors'' --- i.e.\ mappings between abstract
- theories.%
+  constant definitions with recursion over types indirectly provide
+  some kind of ``functors'' --- i.e.\ mappings between abstract
+  theories.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{end}\isamarkupfalse%
+\isacommand{end}\isanewline
+\isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
diff -r 7c6a970f0808 -r de0f4a63baa5 doc-src/AxClass/generated/Product.tex
--- a/doc-src/AxClass/generated/Product.tex	Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/AxClass/generated/Product.tex	Sat Dec 01 18:52:32 2001 +0100
@@ -9,50 +9,49 @@
 %
 \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 \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
- \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.
+  left that we have not yet discussed.  When declaring polymorphic
+  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 \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} is actually an abbreviation
+  for \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}type\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} Since class \isa{type} is the
+  universal class of HOL, this is not really a constraint at all.
 
  The \isa{product} class below provides a less degenerate example of
  syntactic type classes.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{axclass}\isanewline
-\ \ product\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\ \ product\ {\isasymsubseteq}\ type\isanewline
 \isamarkupfalse%
 \isacommand{consts}\isanewline
 \ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
-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.
+Here class \isa{product} is defined as subclass of \isa{type}
+  without any additional axioms.  This effects in logical equivalence
+  of \isa{product} and \isa{type}, as is reflected by the trivial
+  introduction rule generated for this definition.
 
- \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}.
+  \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}type\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} anyway?  In this particular case where \isa{product\ {\isasymequiv}\ type}, 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 \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 $\INSTANCE$ with the default proof $\DDOT$.
+  On the other hand there are syntactic differences, of course.
+  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 $\INSTANCE$ with the default proof $\DDOT$.
 
- \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
- \isa{c}.  Only immediately before \emph{specifying} these constants
- on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}.
+  \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
+  \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 \isa{product} and type \isa{bool} as
- follows.%
+  This is done for class \isa{product} and type \isa{bool} as
+  follows.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product\ \isamarkupfalse%
@@ -85,7 +84,8 @@
  ``providing operations'' or even ``names of functions''.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{end}\isamarkupfalse%
+\isacommand{end}\isanewline
+\isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
diff -r 7c6a970f0808 -r de0f4a63baa5 doc-src/AxClass/generated/Semigroups.tex
--- a/doc-src/AxClass/generated/Semigroups.tex	Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/AxClass/generated/Semigroups.tex	Sat Dec 01 18:52:32 2001 +0100
@@ -9,51 +9,52 @@
 %
 \begin{isamarkuptext}%
 \medskip\noindent An axiomatic type class is simply a class of types
- that all meet certain properties, which are also called \emph{class
- axioms}. Thus, type classes may be also understood as type predicates
- --- i.e.\ abstractions over a single type argument \isa{{\isacharprime}a}.  Class
- axioms typically contain polymorphic constants that depend on this
- type \isa{{\isacharprime}a}.  These \emph{characteristic constants} behave like
- operations associated with the ``carrier'' type \isa{{\isacharprime}a}.
+  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 \isa{{\isacharprime}a}.  Class axioms typically contain polymorphic constants that
+  depend on this 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.%
+  We illustrate these basic concepts by the following formulation of
+  semigroups.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{consts}\isanewline
 \ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ type\isanewline
 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Above we have first declared a polymorphic constant \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and then defined the class \isa{semigroup} of
- 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.
+  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 \isa{{\isacharprime}a} and a fixed
- \emph{signature}.  Different signatures require different classes.
- Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups 
- \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}\isactrlsup {\isasymtau}{\isacharparenright}}, while the original \isa{semigroup} would
- correspond to semigroups of the form \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}\isactrlsup {\isasymtau}{\isacharparenright}}.%
+  \medskip In general, type classes may be used to describe
+  \emph{structures} with exactly one carrier \isa{{\isacharprime}a} and a fixed
+  \emph{signature}.  Different signatures require different classes.
+  Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}\isactrlsup {\isasymtau}{\isacharparenright}}, while the original \isa{semigroup} would
+  correspond to semigroups of the form \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}\isactrlsup {\isasymtau}{\isacharparenright}}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{consts}\isanewline
 \ \ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{axclass}\ plus{\isacharunderscore}semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\isacommand{axclass}\ plus{\isacharunderscore}semigroup\ {\isasymsubseteq}\ type\isanewline
 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent Even if classes \isa{plus{\isacharunderscore}semigroup} and \isa{semigroup} both represent semigroups in a sense, they are certainly
- not quite the same.%
+  not quite the same.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{end}\isamarkupfalse%
+\isacommand{end}\isanewline
+\isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
diff -r 7c6a970f0808 -r de0f4a63baa5 doc-src/TutorialI/Types/Overloading.thy
--- a/doc-src/TutorialI/Types/Overloading.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/TutorialI/Types/Overloading.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -1,13 +1,13 @@
 (*<*)theory Overloading = Overloading1:(*>*)
-instance list :: ("term")ordrel
+instance list :: (type)ordrel
 by intro_classes
 
 text{*\noindent
 This \isacommand{instance} declaration can be read like the declaration of
 a function on types.  The constructor @{text list} maps types of class @{text
-term} (all HOL types), to types of class @{text ordrel};
+type} (all HOL types), to types of class @{text ordrel};
 in other words,
-if @{text"ty :: term"} then @{text"ty list :: ordrel"}.
+if @{text"ty :: type"} then @{text"ty list :: ordrel"}.
 Of course we should also define the meaning of @{text <<=} and
 @{text <<} on lists:
 *}
diff -r 7c6a970f0808 -r de0f4a63baa5 doc-src/TutorialI/Types/Overloading1.thy
--- a/doc-src/TutorialI/Types/Overloading1.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/TutorialI/Types/Overloading1.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -10,13 +10,12 @@
 introduce the class @{text ordrel}:
 *}
 
-axclass ordrel < "term"
+axclass ordrel < type
 
 text{*\noindent
 This introduces a new class @{text ordrel} and makes it a subclass of
-the predefined class @{text term}, which
-is the class of all HOL types.\footnote{The quotes around @{text term}
-simply avoid the clash with the command \isacommand{term}.}
+the predefined class @{text type}, which
+is the class of all HOL types.
 This is a degenerate form of axiomatic type class without any axioms.
 Its sole purpose is to restrict the use of overloaded constants to meaningful
 instances:
diff -r 7c6a970f0808 -r de0f4a63baa5 doc-src/TutorialI/Types/document/Overloading.tex
--- a/doc-src/TutorialI/Types/document/Overloading.tex	Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading.tex	Sat Dec 01 18:52:32 2001 +0100
@@ -2,16 +2,16 @@
 \begin{isabellebody}%
 \def\isabellecontext{Overloading}%
 \isamarkupfalse%
-\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isachardoublequote}term{\isachardoublequote}{\isacharparenright}ordrel\isanewline
+\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}ordrel\isanewline
 \isamarkupfalse%
 \isacommand{by}\ intro{\isacharunderscore}classes\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
 This \isacommand{instance} declaration can be read like the declaration of
-a function on types.  The constructor \isa{list} maps types of class \isa{term} (all HOL types), to types of class \isa{ordrel};
+a function on types.  The constructor \isa{list} maps types of class \isa{type} (all HOL types), to types of class \isa{ordrel};
 in other words,
-if \isa{ty\ {\isacharcolon}{\isacharcolon}\ term} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}.
+if \isa{ty\ {\isacharcolon}{\isacharcolon}\ type} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}.
 Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
 \isa{{\isacharless}{\isacharless}} on lists:%
 \end{isamarkuptext}%
diff -r 7c6a970f0808 -r de0f4a63baa5 doc-src/TutorialI/Types/document/Overloading1.tex
--- a/doc-src/TutorialI/Types/document/Overloading1.tex	Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex	Sat Dec 01 18:52:32 2001 +0100
@@ -14,14 +14,13 @@
 introduce the class \isa{ordrel}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{axclass}\ ordrel\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isamarkupfalse%
+\isacommand{axclass}\ ordrel\ {\isacharless}\ type\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
 This introduces a new class \isa{ordrel} and makes it a subclass of
-the predefined class \isa{term}, which
-is the class of all HOL types.\footnote{The quotes around \isa{term}
-simply avoid the clash with the command \isacommand{term}.}
+the predefined class \isa{type}, which
+is the class of all HOL types.
 This is a degenerate form of axiomatic type class without any axioms.
 Its sole purpose is to restrict the use of overloaded constants to meaningful
 instances:%
diff -r 7c6a970f0808 -r de0f4a63baa5 doc-src/TutorialI/tutorial.ind
--- a/doc-src/TutorialI/tutorial.ind	Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/TutorialI/tutorial.ind	Sat Dec 01 18:52:32 2001 +0100
@@ -90,7 +90,7 @@
   \item bisimulations, 106
   \item \isa {blast} (method), 79--80, 82
   \item \isa {bool} (type), 4, 5
-  \item boolean expressions example, 19--22
+  \item boolean expressions example, 20--22
   \item \isa {bspec} (theorem), \bold{98}
   \item \isacommand{by} (command), 63
 
@@ -213,7 +213,7 @@
   \item flags, 5, 6, 33
     \subitem setting and resetting, 5
   \item \isa {force} (method), 81, 82
-  \item formulae, 5
+  \item formulae, 5--6
   \item forward proof, 82--88
   \item \isa {frule} (method), 73
   \item \isa {frule_tac} (method), 66
@@ -254,7 +254,7 @@
   \item \isa {if} expressions, 5, 6
     \subitem simplification of, 33
     \subitem splitting of, 31, 49
-  \item if-and-only-if, 5
+  \item if-and-only-if, 6
   \item \isa {iff} (attribute), 80, 92, 120
   \item \isa {iffD1} (theorem), \bold{84}
   \item \isa {iffD2} (theorem), \bold{84}
@@ -266,7 +266,7 @@
   \item \isa {impI} (theorem), \bold{62}
   \item implication, 62--63
   \item \isa {ind_cases} (method), 121
-  \item \isa {induct_tac} (method), 12, 19, 52, 178
+  \item \isa {induct_tac} (method), 12, 19, 51, 178
   \item induction, 174--181
     \subitem complete, 176
     \subitem deriving new schemas, 178
@@ -326,7 +326,7 @@
   \item least number operator, \see{\protect\isa{LEAST}}{75}
   \item \isacommand {lemma} (command), 13
   \item \isacommand {lemmas} (command), 83, 92
-  \item \isa {length} (symbol), 17
+  \item \isa {length} (symbol), 18
   \item \isa {length_induct}, \bold{178}
   \item \isa {less_than} (constant), 104
   \item \isa {less_than_iff} (theorem), \bold{104}
@@ -336,9 +336,10 @@
   \item lexicographic product, \bold{105}, 166
   \item {\texttt{lfp}}
     \subitem applications of, \see{CTL}{106}
+  \item Library, 4
   \item linear arithmetic, 22--24, 139
   \item \isa {List} (theory), 17
-  \item \isa {list} (type), 4, 9, 17
+  \item \isa {list} (type), 5, 9, 17
   \item \isa {list.split} (theorem), 32
   \item \isa {lists_mono} (theorem), \bold{127}
   \item Lowe, Gavin, 184--185
@@ -351,7 +352,7 @@
   \item measure functions, 47, 104
   \item \isa {measure_def} (theorem), \bold{105}
   \item meta-logic, \bold{70}
-  \item methods, \bold{15}
+  \item methods, \bold{16}
   \item \isa {min} (constant), 23, 24
   \item \isa {mod} (symbol), 23
   \item \isa {mod_div_equality} (theorem), \bold{141}
@@ -377,8 +378,8 @@
   \item negation, 63--65
   \item \isa {Nil} (constant), 9
   \item \isa {no_asm} (modifier), 29
-  \item \isa {no_asm_simp} (modifier), 29
-  \item \isa {no_asm_use} (modifier), 29
+  \item \isa {no_asm_simp} (modifier), 30
+  \item \isa {no_asm_use} (modifier), 30
   \item non-standard reals, 145
   \item \isa {None} (constant), \bold{24}
   \item \isa {notE} (theorem), \bold{63}
@@ -426,7 +427,7 @@
 
   \indexspace
 
-  \item quantifiers, 5
+  \item quantifiers, 6
     \subitem and inductive definitions, 125--127
     \subitem existential, 72
     \subitem for sets, 98
@@ -483,7 +484,7 @@
 
   \item \isa {safe} (method), 81, 82
   \item safe rules, \bold{80}
-  \item \isa {set} (type), 4, 95
+  \item \isa {set} (type), 5, 95
   \item set comprehensions, 97--98
   \item \isa {set_ext} (theorem), \bold{96}
   \item sets, 95--99
@@ -495,7 +496,7 @@
   \item \isa {simp} (attribute), 11, 28
   \item \isa {simp} (method), \bold{28}
   \item \isa {simp} del (attribute), 28
-  \item \isa {simp_all} (method), 28, 37
+  \item \isa {simp_all} (method), 29, 37
   \item simplification, 27--33, 163--166
     \subitem of \isa{let}-expressions, 31
     \subitem with definitions, 30
@@ -569,7 +570,7 @@
   \item tuples, \see{pairs and tuples}{1}
   \item \isacommand {typ} (command), 16
   \item type constraints, \bold{6}
-  \item type constructors, 4
+  \item type constructors, 5
   \item type inference, \bold{5}
   \item type synonyms, 25
   \item type variables, 5
@@ -597,14 +598,14 @@
     \subitem indexed, 98
   \item \isa {Union_iff} (theorem), \bold{98}
   \item \isa {unit} (type), 24
-  \item unknowns, 6, \bold{58}
+  \item unknowns, 7, \bold{58}
   \item unsafe rules, \bold{80}
   \item updating a function, \bold{99}
 
   \indexspace
 
-  \item variables, 6--7
-    \subitem schematic, 6
+  \item variables, 7
+    \subitem schematic, 7
     \subitem type, 5
   \item \isa {vimage_def} (theorem), \bold{101}
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/AxClasses/Group.thy
--- a/src/HOL/AxClasses/Group.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/AxClasses/Group.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -14,12 +14,12 @@
   one :: 'a
 
 
-axclass monoid < "term"
+axclass monoid < type
   assoc:      "(x [*] y) [*] z = x [*] (y [*] z)"
   left_unit:  "one [*] x = x"
   right_unit: "x [*] one = x"
 
-axclass semigroup < "term"
+axclass semigroup < type
   assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
 
 axclass group < semigroup
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/AxClasses/Product.thy
--- a/src/HOL/AxClasses/Product.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/AxClasses/Product.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -6,7 +6,7 @@
 
 theory Product = Main:
 
-axclass product < "term"
+axclass product < type
 
 consts
   product :: "'a::product => 'a => 'a"    (infixl "[*]" 70)
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/AxClasses/Semigroups.thy
--- a/src/HOL/AxClasses/Semigroups.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/AxClasses/Semigroups.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -9,14 +9,14 @@
 consts
   times :: "'a => 'a => 'a"    (infixl "[*]" 70)
 
-axclass semigroup < "term"
+axclass semigroup < type
   assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
 
 
 consts
   plus :: "'a => 'a => 'a"    (infixl "[+]" 70)
 
-axclass plus_semigroup < "term"
+axclass plus_semigroup < type
   assoc: "(x [+] y) [+] z = x [+] (y [+] z)"
 
 end
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Divides.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -11,7 +11,7 @@
 (*We use the same class for div and mod;
   moreover, dvd is defined whenever multiplication is*)
 axclass
-  div < term
+  div < type
 
 instance  nat :: div
 instance  nat :: plus_ac0 (add_commute,add_assoc,add_0)
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Finite.thy
--- a/src/HOL/Finite.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Finite.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -18,7 +18,7 @@
 syntax finite :: 'a set => bool
 translations  "finite A"  ==  "A : Finites"
 
-axclass	finite<term
+axclass	finite < type
   finite "finite UNIV"
 
 (* This definition, although traditional, is ugly to work with
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Fun.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -373,7 +373,7 @@
   fun mk_eq_cterm sg T l r = Thm.cterm_of sg (equals T $ l $ r)
 in 
   val fun_upd2_simproc = Simplifier.mk_simproc "fun_upd2"
-   [Thm.read_cterm (sign_of (the_context ())) ("f(v:=w,x:=y)", HOLogic.termT)]
+   [HOLogic.read_cterm (sign_of (the_context ())) "f(v := w, x := y)"]
    (fn sg => (K (fn t => case find_double t of (T,None)=> None | (T,Some rhs)=> 
        Some (prove_goalw_cterm [] (mk_eq_cterm sg T t rhs) fun_upd_prover))))
 end;
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Fun.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
 
 Fun = Typedef +
 
-instance set :: (term) order
+instance set :: (type) order
                        (subset_refl,subset_trans,subset_antisym,psubset_eq)
 consts
   fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/HOL.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -13,16 +13,16 @@
 
 subsubsection {* Core syntax *}
 
-global
+classes type < logic
+defaultsort type
 
-classes "term" < logic
-defaultsort "term"
+global
 
 typedecl bool
 
 arities
-  bool :: "term"
-  fun :: ("term", "term") "term"
+  bool :: type
+  fun :: (type, type) type
 
 judgment
   Trueprop      :: "bool => prop"                   ("(_)" 5)
@@ -145,12 +145,12 @@
 
 subsubsection {* Generic algebraic operations *}
 
-axclass zero < "term"
-axclass one < "term"
-axclass plus < "term"
-axclass minus < "term"
-axclass times < "term"
-axclass inverse < "term"
+axclass zero < type
+axclass one < type
+axclass plus < type
+axclass minus < type
+axclass times < type
+axclass inverse < type
 
 global
 
@@ -528,7 +528,7 @@
 subsection {* Order signatures and orders *}
 
 axclass
-  ord < "term"
+  ord < type
 
 syntax
   "op <"        :: "['a::ord, 'a] => bool"             ("op <")
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/IMP/Com.thy
--- a/src/HOL/IMP/Com.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/IMP/Com.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -16,7 +16,7 @@
       aexp  = state => val
       bexp  = state => bool
 
-arities loc :: term
+arities loc :: type
 
 datatype
   com = SKIP
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/IMP/Expr.thy
--- a/src/HOL/IMP/Expr.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/IMP/Expr.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -15,7 +15,7 @@
       n2n = "nat => nat"
       n2n2n = "nat => nat => nat"
 
-arities loc :: term
+arities loc :: type
 
 datatype
   aexp = N nat
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/IMPP/Com.thy
--- a/src/HOL/IMPP/Com.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/IMPP/Com.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -12,7 +12,7 @@
                         current Isabelle, types cannot be refined later *)
 types	 glb
          loc
-arities	 (*val,*)glb,loc :: term
+arities	 (*val,*)glb,loc :: type
 consts   Arg, Res :: loc
 
 datatype vname  = Glb glb | Loc loc
@@ -21,14 +21,14 @@
 datatype state  = st globs locals
 (* for the meta theory, the following would be sufficient:
 types    state
-arities  state::term
+arities  state::type
 consts   st:: [globs , locals] => state
 *)
 types	 aexp   = state => val
 	 bexp   = state => bool
 
 types	pname
-arities	pname  :: term
+arities	pname  :: type
 
 datatype com
       = SKIP
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Induct/Com.thy
--- a/src/HOL/Induct/Com.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Induct/Com.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -12,7 +12,7 @@
       state = "loc => nat"
       n2n2n = "nat => nat => nat"
 
-arities loc :: term
+arities loc :: type
 
 datatype
   exp = N nat
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Integ/Bin.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -349,7 +349,7 @@
   fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg []
 
   fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc
-  fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.termT)
+  fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context())) s
   val prep_pats = map prep_pat
 
   fun is_numeral (Const("Numeral.number_of", _) $ w) = true
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -169,8 +169,7 @@
                 bin_arith_simps @ bin_rel_simps;
 
 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
-fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ()))
-                                (s, HOLogic.termT);
+fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context ())) s;
 val prep_pats = map prep_pat;
 
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Lattice/Lattice.thy
--- a/src/HOL/Lattice/Lattice.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Lattice/Lattice.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -519,7 +519,7 @@
   qed
 qed
 
-instance fun :: ("term", lattice) lattice
+instance fun :: (type, lattice) lattice
 proof
   fix f g :: "'a \<Rightarrow> 'b::lattice"
   show "\<exists>inf. is_inf f g inf" by rule (rule is_inf_fun) (* FIXME @{text "from \<dots> show \<dots> .."} does not work!? unification incompleteness!? *)
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Lattice/Orders.thy
--- a/src/HOL/Lattice/Orders.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Lattice/Orders.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -18,7 +18,7 @@
   required to be related (in either direction).
 *}
 
-axclass leq < "term"
+axclass leq < type
 consts
   leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "[=" 50)
 syntax (xsymbols)
@@ -249,7 +249,7 @@
   orders need \emph{not} be linear in general.
 *}
 
-instance fun :: ("term", leq) leq ..
+instance fun :: (type, leq) leq ..
 
 defs (overloaded)
   leq_fun_def: "f \<sqsubseteq> g \<equiv> \<forall>x. f x \<sqsubseteq> g x"
@@ -260,7 +260,7 @@
 lemma leq_funD [dest?]: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
   by (unfold leq_fun_def) blast
 
-instance fun :: ("term", quasi_order) quasi_order
+instance fun :: (type, quasi_order) quasi_order
 proof
   fix f g h :: "'a \<Rightarrow> 'b::quasi_order"
   show "f \<sqsubseteq> f"
@@ -276,7 +276,7 @@
   qed
 qed
 
-instance fun :: ("term", partial_order) partial_order
+instance fun :: (type, partial_order) partial_order
 proof
   fix f g :: "'a \<Rightarrow> 'b::partial_order"
   assume fg: "f \<sqsubseteq> g" and gf: "g \<sqsubseteq> f"
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -13,13 +13,13 @@
 
 subsection {* Prefix order on lists *}
 
-instance list :: ("term") ord ..
+instance list :: (type) ord ..
 
 defs (overloaded)
   prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs"
   strict_prefix_def: "xs < ys == xs \<le> ys \<and> xs \<noteq> (ys::'a list)"
 
-instance list :: ("term") order
+instance list :: (type) order
   by intro_classes (auto simp add: prefix_def strict_prefix_def)
 
 lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -47,9 +47,9 @@
   set_of :: "'a multiset => 'a set"
   "set_of M == {x. x :# M}"
 
-instance multiset :: ("term") plus ..
-instance multiset :: ("term") minus ..
-instance multiset :: ("term") zero ..
+instance multiset :: (type) plus ..
+instance multiset :: (type) minus ..
+instance multiset :: (type) zero ..
 
 defs (overloaded)
   union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
@@ -114,7 +114,7 @@
 
 theorems union_ac = union_assoc union_commute union_lcomm
 
-instance multiset :: ("term") plus_ac0
+instance multiset :: (type) plus_ac0
   apply intro_classes
     apply (rule union_commute)
    apply (rule union_assoc)
@@ -660,7 +660,7 @@
 
 subsubsection {* Partial-order properties *}
 
-instance multiset :: ("term") ord ..
+instance multiset :: (type) ord ..
 
 defs (overloaded)
   less_multiset_def: "M' < M == (M', M) \<in> mult {(x', x). x' < x}"
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Library/Quotient.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -23,7 +23,7 @@
  "\<sim> :: 'a => 'a => bool"}.
 *}
 
-axclass eqv \<subseteq> "term"
+axclass eqv \<subseteq> type
 consts
   eqv :: "('a::eqv) => 'a => bool"    (infixl "\<sim>" 50)
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/MicroJava/J/Type.thy
--- a/src/HOL/MicroJava/J/Type.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/MicroJava/J/Type.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -11,9 +11,6 @@
 typedecl cname  (* class name *)
 typedecl vnam   (* variable or field name *)
 typedecl mname  (* method name *)
-arities  cname :: "term"
-         vnam  :: "term"
-         mname :: "term"
 
 datatype vname    (* names for This pointer and local/field variables *)
   = This
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/MicroJava/J/Value.thy
--- a/src/HOL/MicroJava/J/Value.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/MicroJava/J/Value.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -9,7 +9,6 @@
 theory Value = Type:
 
 typedecl loc (* locations, i.e. abstract references on objects *)
-arities loc :: "term"
 
 datatype val
   = Unit        (* dummy result value of void methods *)
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/MiniML/Type.thy
--- a/src/HOL/MiniML/Type.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/MiniML/Type.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -9,7 +9,7 @@
 Type = Maybe + 
 
 (* new class for structures containing type variables *)
-axclass  type_struct < term 
+axclass  type_struct < type
 
 
 (* type expressions *)
@@ -33,7 +33,7 @@
 instance  typ::type_struct
 instance  type_scheme::type_struct  
 instance  list::(type_struct)type_struct
-instance  fun::(term,type_struct)type_struct
+instance  fun::(type,type_struct)type_struct
 
 
 (* free_tv s: the type variables occuring freely in the type structure s *)
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Nat.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -19,7 +19,7 @@
 instance nat :: linorder (nat_le_linear)
 instance nat :: wellorder (wf_less)
 
-axclass power < term
+axclass power < type
 
 consts
   power :: ['a::power, nat] => 'a            (infixr "^" 80)
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/NatDef.thy
--- a/src/HOL/NatDef.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/NatDef.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -12,13 +12,8 @@
 
 (** type ind **)
 
-global
-
-types
-  ind
-
-arities
-  ind :: term
+types ind
+arities ind :: type
 
 consts
   Zero_Rep      :: ind
@@ -43,6 +38,8 @@
   Zero_RepI "Zero_Rep : Nat'"
   Suc_RepI  "i : Nat' ==> Suc_Rep i : Nat'"
 
+global
+
 typedef (Nat)
   nat = "Nat'"   (Nat'.Zero_RepI)
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Numeral.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -14,7 +14,7 @@
       | Bit bin bool    (infixl "BIT" 90)
 
 axclass
-  number < "term"      (*for numeric types: nat, int, real, ...*)
+  number < type  -- {* for numeric types: nat, int, real, \dots *}
 
 consts
   number_of :: "bin => 'a::number"
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Product_Type.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -342,8 +342,8 @@
         (cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
         (K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
   val sign = sign_of (the_context ());
-  fun simproc name patstr = Simplifier.mk_simproc name
-                [Thm.read_cterm sign (patstr, HOLogic.termT)];
+  fun simproc name patstr =
+    Simplifier.mk_simproc name [HOLogic.read_cterm sign patstr];
 
   val beta_patstr = "split f z";
   val  eta_patstr = "split f";
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Prolog/Func.thy
--- a/src/HOL/Prolog/Func.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Prolog/Func.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -4,7 +4,7 @@
 
 types tm
 
-arities tm :: term
+arities tm :: type
 
 consts	abs	:: (tm => tm) => tm
 	app	:: tm => tm => tm
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Prolog/Test.thy
--- a/src/HOL/Prolog/Test.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Prolog/Test.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -3,10 +3,10 @@
 Test = HOHH +
 
 types nat
-arities nat :: term
+arities nat :: type
 
 types 'a list
-arities list :: (term) term
+arities list :: (type) type
 
 consts Nil   :: 'a list		 	 		 ("[]")
        Cons  :: 'a => 'a list => 'a list		 (infixr "#"  65)
@@ -20,7 +20,7 @@
   "[x]"         == "x#[]"
 
 types   person
-arities person  :: term
+arities person  :: type
 
 consts  
 	append  :: ['a list, 'a list, 'a list]		  => bool
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Prolog/Type.thy
--- a/src/HOL/Prolog/Type.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Prolog/Type.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -4,7 +4,7 @@
 
 types ty
 
-arities ty :: term
+arities ty :: type
 
 consts  bool	:: ty
 	nat	:: ty
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Real/RealBin.ML
--- a/src/HOL/Real/RealBin.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Real/RealBin.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -403,7 +403,7 @@
  	  real_mult_0, real_mult_0_right, real_mult_1, real_mult_1_right];
 
 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
-fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.termT);
+fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context ())) s;
 val prep_pats = map prep_pat;
 
 structure CancelNumeralsCommon =
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Relation_Power.thy
--- a/src/HOL/Relation_Power.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Relation_Power.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -15,7 +15,7 @@
 Relation_Power = Nat +
 
 instance
-  set :: (term) {power}   (* only ('a * 'a) set should be in power! *)
+  set :: (type) power   (* only ('a * 'a) set should be in power! *)
 
 primrec (relpow)
   "R^0 = Id"
@@ -23,7 +23,7 @@
 
 
 instance
-  fun :: (term,term)power   (* only 'a => 'a should be in power! *)
+  fun :: (type, type) power   (* only 'a => 'a should be in power! *)
 
 primrec (funpow)
   "f^0 = id"
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Set.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -17,7 +17,7 @@
 global
 
 typedecl 'a set
-arities set :: ("term") "term"
+arities set :: (type) type
 
 consts
   "{}"          :: "'a set"                             ("{}")
@@ -42,8 +42,8 @@
 
 local
 
-instance set :: ("term") ord ..
-instance set :: ("term") minus ..
+instance set :: (type) ord ..
+instance set :: (type) minus ..
 
 
 subsection {* Additional concrete syntax *}
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/TLA/Init.thy
--- a/src/HOL/TLA/Init.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/TLA/Init.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -17,7 +17,7 @@
   temporal = behavior form
 
 arities
-  behavior    :: term
+  behavior    :: type
 
 instance
   behavior    :: world
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/TLA/Intensional.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -13,12 +13,12 @@
 Intensional  =  Main +
 
 axclass
-  world < term
+  world < type
 
 (** abstract syntax **)
 
 types
-  ('w,'a) expr = 'w => 'a               (* intention: 'w::world, 'a::term *)
+  ('w,'a) expr = 'w => 'a               (* intention: 'w::world, 'a::type *)
   'w form = ('w, bool) expr
 
 consts
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/TLA/Memory/ProcedureInterface.thy
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -21,7 +21,7 @@
   ('a,'r) channel = (PrIds => ('a,'r) chan) stfun
 
 arities
-  chan :: (term,term) term
+  chan :: (type,type) type
 
 consts
   (* data-level functions *)
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/TLA/Stfun.thy
--- a/src/HOL/TLA/Stfun.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/TLA/Stfun.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -17,7 +17,7 @@
     stpred   = "bool stfun"
 
 arities
-  state :: term
+  state :: type
 
 instance
   state :: world
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -120,7 +120,7 @@
           (1 upto (length descr'))));
 
     val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
-      replicate (length descr') HOLogic.termS);
+      replicate (length descr') HOLogic.typeS);
 
     val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
@@ -302,7 +302,7 @@
     val recTs = get_rec_types descr' sorts;
     val used = foldr add_typ_tfree_names (recTs, []);
     val newTs = take (length (hd descr), recTs);
-    val T' = TFree (variant used "'t", HOLogic.termS);
+    val T' = TFree (variant used "'t", HOLogic.typeS);
 
     fun mk_dummyT (DtRec _) = T'
       | mk_dummyT (DtType ("fun", [T, _])) = typ_of_dtyp descr' sorts T --> T'
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -365,7 +365,7 @@
    | _ => None)
   | distinct_proc sg _ _ = None;
 
-val distinct_pats = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s = t", HOLogic.termT)];
+val distinct_pats = [HOLogic.read_cterm (Theory.sign_of HOL.thy) "s = t"];
 val distinct_simproc = mk_simproc distinctN distinct_pats distinct_proc;
 
 val dist_ss = HOL_ss addsimprocs [distinct_simproc];
@@ -460,7 +460,7 @@
           (constrs ~~ constr_syntax')) ((hd descr) ~~ newTs ~~ constr_syntax);
 
     val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
-      replicate (length descr') HOLogic.termS);
+      replicate (length descr') HOLogic.typeS);
 
     val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
@@ -484,7 +484,7 @@
     val size_names = DatatypeProp.indexify_names
       (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs)));
 
-    val freeT = TFree (variant used "'t", HOLogic.termS);
+    val freeT = TFree (variant used "'t", HOLogic.typeS);
     val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
         let val Ts = map (typ_of_dtyp descr' sorts) cargs
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Tools/datatype_prop.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -177,7 +177,7 @@
     val used = foldr add_typ_tfree_names (recTs, []);
 
     val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
-      replicate (length descr') HOLogic.termS);
+      replicate (length descr') HOLogic.typeS);
 
     val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
@@ -241,7 +241,7 @@
     val recTs = get_rec_types descr' sorts;
     val used = foldr add_typ_tfree_names (recTs, []);
     val newTs = take (length (hd descr), recTs);
-    val T' = TFree (variant used "'t", HOLogic.termS);
+    val T' = TFree (variant used "'t", HOLogic.typeS);
 
     val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
@@ -326,7 +326,7 @@
     val recTs = get_rec_types descr' sorts;
     val used' = foldr add_typ_tfree_names (recTs, []);
     val newTs = take (length (hd descr), recTs);
-    val T' = TFree (variant used' "'t", HOLogic.termS);
+    val T' = TFree (variant used' "'t", HOLogic.typeS);
     val P = Free ("P", T' --> HOLogic.boolT);
 
     fun make_split (((_, (_, _, constrs)), T), comb_t) =
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -838,7 +838,7 @@
 fun add_inductive verbose coind c_strings intro_srcs raw_monos thy =
   let
     val sign = Theory.sign_of thy;
-    val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
+    val cs = map (term_of o HOLogic.read_cterm sign) c_strings;
 
     val intr_names = map (fst o fst) intro_srcs;
     fun read_rule s = Thm.read_cterm sign (s, propT)
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Tools/record_package.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -493,7 +493,7 @@
 
 local
 
-val sel_upd_pat = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s (u k r)", HOLogic.termT)];
+val sel_upd_pat = [HOLogic.read_cterm (Theory.sign_of HOL.thy) "s (u k r)"];
 
 fun proc sg _ t =
   (case t of (sel as Const (s, _)) $ ((upd as Const (u, _)) $ k $ r) =>
@@ -560,7 +560,7 @@
 fun field_typedefs zeta moreT names theory =
   let
     val alpha = "'a";
-    val aT = TFree (alpha, HOLogic.termS);
+    val aT = TFree (alpha, HOLogic.typeS);
     val UNIV = HOLogic.mk_UNIV (HOLogic.mk_prodT (aT, moreT));
 
     fun type_def (thy, name) =
@@ -581,7 +581,7 @@
     val base = Sign.base_name;
     val full_path = Sign.full_name_path sign;
 
-    val xT = TFree (variant alphas "'x", HOLogic.termS);
+    val xT = TFree (variant alphas "'x", HOLogic.typeS);
 
 
     (* prepare declarations and definitions *)
@@ -683,7 +683,7 @@
     val all_named_vars = parent_named_vars @ named_vars;
 
     val zeta = variant alphas "'z";
-    val moreT = TFree (zeta, HOLogic.termS);
+    val moreT = TFree (zeta, HOLogic.typeS);
     val more = Free (moreN, moreT);
     val full_moreN = full moreN;
     fun more_part t = mk_more t full_moreN;
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -58,7 +58,7 @@
     val full = Sign.full_name (Theory.sign_of thy);
 
     fun arity_of (raw_name, args, mx) =
-      (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.termS, HOLogic.termS);
+      (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.typeS, HOLogic.typeS);
   in
     if can (Theory.assert_super HOL.thy) thy then
       thy
@@ -97,7 +97,7 @@
 (* prepare_typedef *)
 
 fun read_term sg used s =
-  #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.termT));
+  #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.typeT));
 
 fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg;
 
@@ -125,7 +125,7 @@
     val goal_pat = mk_nonempty (Var (vname, setT));
 
     (*lhs*)
-    val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs;
+    val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.typeS)) vs;
     val tname = Syntax.type_name t mx;
     val full_tname = full tname;
     val newT = Type (full_tname, map TFree lhs_tfrees);
@@ -162,7 +162,9 @@
           fun make th = Drule.standard (th OF [type_definition]);
           val (theory'', [Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
               Rep_cases, Abs_cases, Rep_induct, Abs_induct]) =
-            theory' |> PureThy.add_thms
+            theory'
+            |> Theory.add_path name
+            |> PureThy.add_thms
               ([((Rep_name, make Rep), []),
                 ((Rep_name ^ "_inverse", make Rep_inverse), []),
                 ((Abs_name ^ "_inverse", make Abs_inverse), []),
@@ -175,7 +177,8 @@
                 ((Rep_name ^ "_induct", make Rep_induct),
                   [RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]),
                 ((Abs_name ^ "_induct", make Abs_induct),
-                  [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])]);
+                  [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])])
+            |>> Theory.parent_path;
           val result = {type_definition = type_definition, set_def = set_def,
             Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
             Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/UNITY/Comp.thy
--- a/src/HOL/UNITY/Comp.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/UNITY/Comp.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -16,7 +16,7 @@
 Comp = Union +
 
 instance
-  program :: (term)ord
+  program :: (type) ord
 
 defs
   component_def   "F <= H == EX G. F Join G = H"
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/UNITY/Comp/Counterc.thy
--- a/src/HOL/UNITY/Comp/Counterc.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/UNITY/Comp/Counterc.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -13,7 +13,7 @@
 
 Counterc =  Comp +
 types state
-arities state :: term
+arities state :: type
 
 consts
   C :: "state=>int"
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/UNITY/Comp/PriorityAux.thy
--- a/src/HOL/UNITY/Comp/PriorityAux.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/UNITY/Comp/PriorityAux.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -6,10 +6,10 @@
 Auxiliary definitions needed in Priority.thy
 *)
 
-PriorityAux  =  Main +
+PriorityAux = Main +
 
 types vertex
-arities vertex::term
+arities vertex :: type
   
 constdefs
   (* symmetric closure: removes the orientation of a relation *)
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/UNITY/Extend.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -125,7 +125,7 @@
 
 (** A sequence of proof steps borrowed from Provers/split_paired_all.ML **)
 
-val cT = TFree ("'c", ["term"]);
+val cT = TFree ("'c", HOLogic.typeS);
 
 (* "PROP P x == PROP P (h (f x, g x))" *)
 val lemma1 = Thm.combination
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/UNITY/GenPrefix.thy
--- a/src/HOL/UNITY/GenPrefix.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/UNITY/GenPrefix.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -27,7 +27,7 @@
 
     append  "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)"
 
-instance list :: (term)ord
+instance list :: (type)ord
 
 defs
   prefix_def        "xs <= zs  ==  (xs,zs) : genPrefix Id"
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/UNITY/Guar.thy
--- a/src/HOL/UNITY/Guar.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/UNITY/Guar.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -20,7 +20,7 @@
 
 Guar = Comp +
 
-instance program :: (term) order
+instance program :: (type) order
                     (component_refl, component_trans, component_antisym,
                      program_less_le)
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/UNITY/ListOrder.thy
--- a/src/HOL/UNITY/ListOrder.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/UNITY/ListOrder.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
 
 ListOrder = GenPrefix +
 
-instance list :: (term) order
+instance list :: (type) order
     (prefix_refl,prefix_trans,prefix_antisym,prefix_less_le)
 
 end
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/UNITY/Simple/Reach.thy
--- a/src/HOL/UNITY/Simple/Reach.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/UNITY/Simple/Reach.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -11,7 +11,7 @@
 types   vertex
         state = "vertex=>bool"
 
-arities vertex :: term
+arities vertex :: type
 
 consts
   init ::  "vertex"
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/W0/Type.thy
--- a/src/HOL/W0/Type.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/W0/Type.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -10,7 +10,7 @@
 
 (* new class for structures containing type variables *)
 classes
-        type_struct < term 
+        type_struct < type
 
 (* type expressions *)
 datatype
@@ -23,7 +23,7 @@
 arities
         typ::type_struct
         list::(type_struct)type_struct
-        fun::(term,type_struct)type_struct
+        fun::(type,type_struct)type_struct
 
 (* substitutions *)
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/arith_data.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -138,8 +138,7 @@
 
 (** prepare nat_cancel simprocs **)
 
-fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) 
-                                (s, HOLogic.termT);
+fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context ())) s;
 val prep_pats = map prep_pat;
 
 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/ex/MT.thy
--- a/src/HOL/ex/MT.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/ex/MT.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -31,19 +31,19 @@
   TyEnv
 
 arities 
-  Const :: term
+  Const :: type
 
-  ExVar :: term
-  Ex :: term
+  ExVar :: type
+  Ex :: type
 
-  TyConst :: term
-  Ty :: term
+  TyConst :: type
+  Ty :: type
 
-  Clos :: term
-  Val :: term
+  Clos :: type
+  Val :: type
 
-  ValEnv :: term
-  TyEnv :: term
+  ValEnv :: type
+  TyEnv :: type
 
 consts
   c_app :: [Const, Const] => Const
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/ex/PER.thy
--- a/src/HOL/ex/PER.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/ex/PER.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -8,39 +8,40 @@
 theory PER = Main:
 
 text {*
- Higher-order quotients are defined over partial equivalence relations
- (PERs) instead of total ones.  We provide axiomatic type classes
- @{text "equiv < partial_equiv"} and a type constructor
- @{text "'a quot"} with basic operations.  This development is based
- on:
+  Higher-order quotients are defined over partial equivalence
+  relations (PERs) instead of total ones.  We provide axiomatic type
+  classes @{text "equiv < partial_equiv"} and a type constructor
+  @{text "'a quot"} with basic operations.  This development is based
+  on:
 
- Oscar Slotosch: \emph{Higher Order Quotients and their Implementation
- in Isabelle HOL.}  Elsa L. Gunter and Amy Felty, editors, Theorem
- Proving in Higher Order Logics: TPHOLs '97, Springer LNCS 1275, 1997.
+  Oscar Slotosch: \emph{Higher Order Quotients and their
+  Implementation in Isabelle HOL.}  Elsa L. Gunter and Amy Felty,
+  editors, Theorem Proving in Higher Order Logics: TPHOLs '97,
+  Springer LNCS 1275, 1997.
 *}
 
 
 subsection {* Partial equivalence *}
 
 text {*
- Type class @{text partial_equiv} models partial equivalence relations
- (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation,
- which is required to be symmetric and transitive, but not necessarily
- reflexive.
+  Type class @{text partial_equiv} models partial equivalence
+  relations (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a =>
+  bool"} relation, which is required to be symmetric and transitive,
+  but not necessarily reflexive.
 *}
 
 consts
   eqv :: "'a => 'a => bool"    (infixl "\<sim>" 50)
 
-axclass partial_equiv < "term"
+axclass partial_equiv < type
   partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
   partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
 
 text {*
- \medskip The domain of a partial equivalence relation is the set of
- reflexive elements.  Due to symmetry and transitivity this
- characterizes exactly those elements that are connected with
- \emph{any} other one.
+  \medskip The domain of a partial equivalence relation is the set of
+  reflexive elements.  Due to symmetry and transitivity this
+  characterizes exactly those elements that are connected with
+  \emph{any} other one.
 *}
 
 constdefs
@@ -64,9 +65,9 @@
 subsection {* Equivalence on function spaces *}
 
 text {*
- The @{text \<sim>} relation is lifted to function spaces.  It is
- important to note that this is \emph{not} the direct product, but a
- structural one corresponding to the congruence property.
+  The @{text \<sim>} relation is lifted to function spaces.  It is
+  important to note that this is \emph{not} the direct product, but a
+  structural one corresponding to the congruence property.
 *}
 
 defs (overloaded)
@@ -81,8 +82,8 @@
   by (unfold eqv_fun_def) blast
 
 text {*
- The class of partial equivalence relations is closed under function
- spaces (in \emph{both} argument positions).
+  The class of partial equivalence relations is closed under function
+  spaces (in \emph{both} argument positions).
 *}
 
 instance fun :: (partial_equiv, partial_equiv) partial_equiv
@@ -113,18 +114,18 @@
 subsection {* Total equivalence *}
 
 text {*
- The class of total equivalence relations on top of PERs.  It
- coincides with the standard notion of equivalence, i.e.\
- @{text "\<sim> :: 'a => 'a => bool"} is required to be reflexive, transitive
- and symmetric.
+  The class of total equivalence relations on top of PERs.  It
+  coincides with the standard notion of equivalence, i.e.\ @{text "\<sim>
+  :: 'a => 'a => bool"} is required to be reflexive, transitive and
+  symmetric.
 *}
 
 axclass equiv < partial_equiv
   eqv_refl [intro]: "x \<sim> x"
 
 text {*
- On total equivalences all elements are reflexive, and congruence
- holds unconditionally.
+  On total equivalences all elements are reflexive, and congruence
+  holds unconditionally.
 *}
 
 theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain"
@@ -145,8 +146,8 @@
 subsection {* Quotient types *}
 
 text {*
- The quotient type @{text "'a quot"} consists of all \emph{equivalence
- classes} over elements of the base type @{typ 'a}.
+  The quotient type @{text "'a quot"} consists of all
+  \emph{equivalence classes} over elements of the base type @{typ 'a}.
 *}
 
 typedef 'a quot = "{{x. a \<sim> x}| a::'a. True}"
@@ -159,8 +160,8 @@
   by (unfold quot_def) blast
 
 text {*
- \medskip Abstracted equivalence classes are the canonical
- representation of elements of a quotient type.
+  \medskip Abstracted equivalence classes are the canonical
+  representation of elements of a quotient type.
 *}
 
 constdefs
@@ -183,8 +184,8 @@
 subsection {* Equality on quotients *}
 
 text {*
- Equality of canonical quotient elements corresponds to the original
- relation as follows.
+  Equality of canonical quotient elements corresponds to the original
+  relation as follows.
 *}
 
 theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/hologic.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -7,9 +7,9 @@
 
 signature HOLOGIC =
 sig
-  val termC: class
-  val termS: sort
-  val termT: typ
+  val typeS: sort
+  val typeT: typ
+  val read_cterm: Sign.sg -> string -> cterm
   val boolN: string
   val boolT: typ
   val false_const: term
@@ -80,11 +80,12 @@
 structure HOLogic: HOLOGIC =
 struct
 
-(* basics *)
+(* HOL syntax *)
 
-val termC: class = "term";
-val termS: sort = [termC];
-val termT = TypeInfer.anyT termS;
+val typeS: sort = ["HOL.type"];
+val typeT = TypeInfer.anyT typeS;
+
+fun read_cterm sg s = Thm.read_cterm sg (s, typeT);
 
 
 (* bool and set *)
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/Discrete.ML
--- a/src/HOLCF/Discrete.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Discrete.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -10,11 +10,11 @@
 Addsimps [undiscr_Discr];
 
 Goal
- "!!S::nat=>('a::term)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
+ "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
 by (fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
 qed "discr_chain_f_range0";
 
-Goalw [cont,is_lub_def,is_ub_def] "cont(%x::('a::term)discr. f x)";
+Goalw [cont,is_lub_def,is_ub_def] "cont(%x::('a::type)discr. f x)";
 by (simp_tac (simpset() addsimps [discr_chain_f_range0]) 1);
 qed "cont_discr";
 AddIffs [cont_discr];
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/Discrete.thy
--- a/src/HOLCF/Discrete.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Discrete.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -8,10 +8,10 @@
 
 Discrete = Discrete1 +
 
-instance discr :: (term)cpo   (discr_cpo)
+instance discr :: (type)cpo   (discr_cpo)
 
 constdefs
-   undiscr :: ('a::term)discr => 'a
+   undiscr :: ('a::type)discr => 'a
   "undiscr x == (case x of Discr y => y)"
 
 end
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/Discrete0.ML
--- a/src/HOLCF/Discrete0.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Discrete0.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -6,17 +6,17 @@
 Proves that 'a discr is a po
 *)
 
-Goalw [less_discr_def] "(x::('a::term)discr) << x";
+Goalw [less_discr_def] "(x::('a::type)discr) << x";
 by (rtac refl 1);
 qed "less_discr_refl";
 
 Goalw [less_discr_def]
-  "!!x. [| (x::('a::term)discr) << y; y << z |] ==> x <<  z";
+  "!!x. [| (x::('a::type)discr) << y; y << z |] ==> x <<  z";
 by (etac trans 1);
 by (assume_tac 1);
 qed "less_discr_trans";
 
 Goalw [less_discr_def]
-  "!!x. [| (x::('a::term)discr) << y; y << x |] ==> x=y";
+  "!!x. [| (x::('a::type)discr) << y; y << x |] ==> x=y";
 by (assume_tac 1);
 qed "less_discr_antisym";
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/Discrete0.thy
--- a/src/HOLCF/Discrete0.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Discrete0.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -8,11 +8,11 @@
 
 Discrete0 = Cont + Datatype +
 
-datatype 'a discr = Discr "'a :: term"
+datatype 'a discr = Discr "'a :: type"
 
-instance discr :: (term)sq_ord
+instance discr :: (type) sq_ord
 
 defs
-less_discr_def "((op <<)::('a::term)discr=>'a discr=>bool)  ==  op ="
+less_discr_def "((op <<)::('a::type)discr=>'a discr=>bool)  ==  op ="
 
 end
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/Discrete1.ML
--- a/src/HOLCF/Discrete1.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Discrete1.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -6,13 +6,13 @@
 Proves that 'a discr is a cpo
 *)
 
-Goalw [less_discr_def] "((x::('a::term)discr) << y) = (x=y)";
+Goalw [less_discr_def] "((x::('a::type)discr) << y) = (x=y)";
 by (rtac refl 1);
 qed "discr_less_eq";
 AddIffs [discr_less_eq];
 
 Goalw [chain_def]
- "!!S::nat=>('a::term)discr. chain S ==> S i = S 0";
+ "!!S::nat=>('a::type)discr. chain S ==> S i = S 0";
 by (induct_tac "i" 1);
 by (rtac refl 1);
 by (etac subst 1);
@@ -21,12 +21,12 @@
 qed "discr_chain0";
 
 Goal
- "!!S::nat=>('a::term)discr. chain(S) ==> range(S) = {S 0}";
+ "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}";
 by (fast_tac (claset() addEs [discr_chain0]) 1);
 qed "discr_chain_range0";
 Addsimps [discr_chain_range0];
 
 Goalw [is_lub_def,is_ub_def]
- "!!S. chain S ==> ? x::('a::term)discr. range(S) <<| x";
+ "!!S. chain S ==> ? x::('a::type)discr. range(S) <<| x";
 by (Asm_simp_tac 1);
 qed "discr_cpo";
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/Discrete1.thy
--- a/src/HOLCF/Discrete1.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Discrete1.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
 
 Discrete1 = Discrete0 +
 
-instance discr :: (term)po
+instance discr :: (type) po
   (less_discr_refl,less_discr_trans,less_discr_antisym)
 
 end
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/FOCUS/Buffer.thy
--- a/src/HOLCF/FOCUS/Buffer.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/FOCUS/Buffer.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -21,7 +21,7 @@
 Buffer = FOCUS + 
 
 types   D
-arities D::term
+arities D :: type
 
 datatype
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/FOCUS/Fstream.thy
--- a/src/HOLCF/FOCUS/Fstream.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/FOCUS/Fstream.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -10,7 +10,7 @@
 
 Fstream = Stream + 
 
-default term
+default type
 
 types 'a fstream = ('a lift) stream
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/Fun1.ML
--- a/src/HOLCF/Fun1.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Fun1.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -10,19 +10,19 @@
 (* less_fun is a partial order on 'a => 'b                                  *)
 (* ------------------------------------------------------------------------ *)
 
-val prems = goalw thy [less_fun_def] "(f::'a::term =>'b::po) << f";
+val prems = goalw thy [less_fun_def] "(f::'a::type =>'b::po) << f";
 by (fast_tac (HOL_cs addSIs [refl_less]) 1);
 qed "refl_less_fun";
 
 val prems = goalw Fun1.thy [less_fun_def] 
-        "[|(f1::'a::term =>'b::po) << f2; f2 << f1|] ==> f1 = f2";
+        "[|(f1::'a::type =>'b::po) << f2; f2 << f1|] ==> f1 = f2";
 by (cut_facts_tac prems 1);
 by (stac expand_fun_eq 1);
 by (fast_tac (HOL_cs addSIs [antisym_less]) 1);
 qed "antisym_less_fun";
 
 val prems = goalw Fun1.thy [less_fun_def] 
-        "[|(f1::'a::term =>'b::po) << f2; f2 << f3 |] ==> f1 << f3";
+        "[|(f1::'a::type =>'b::po) << f2; f2 << f3 |] ==> f1 << f3";
 by (cut_facts_tac prems 1);
 by (strip_tac 1);
 by (rtac trans_less 1);
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/Fun1.thy
--- a/src/HOLCF/Fun1.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Fun1.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -13,7 +13,7 @@
 instance flat<chfin (flat_imp_chfin)
 
 (* to make << defineable: *)
-instance fun  :: (term,sq_ord)sq_ord
+instance fun  :: (type, sq_ord) sq_ord
 
 defs
   less_fun_def "(op <<) == (%f1 f2.!x. f1 x << f2 x)"  
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/Fun2.ML
--- a/src/HOLCF/Fun2.ML	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Fun2.ML	Sat Dec 01 18:52:32 2001 +0100
@@ -2,8 +2,6 @@
     ID:         $Id$
     Author:     Franz Regensburger
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
-
-Class Instance =>::(term,po)po
 *)
 
 (* for compatibility with old HOLCF-Version *)
@@ -13,7 +11,7 @@
 qed "inst_fun_po";
 
 (* ------------------------------------------------------------------------ *)
-(* Type 'a::term => 'b::pcpo is pointed                                     *)
+(* Type 'a::type => 'b::pcpo is pointed                                     *)
 (* ------------------------------------------------------------------------ *)
 
 Goal "(%z. UU) << x";
@@ -48,7 +46,7 @@
 (* upper bounds of function chains yield upper bound in the po range        *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "range(S::nat=>('a::term => 'b::po)) <| u ==> range(%i. S i x) <| u(x)";
+Goal "range(S::nat=>('a::type => 'b::po)) <| u ==> range(%i. S i x) <| u(x)";
 by (rtac ub_rangeI 1);
 by (dtac ub_rangeD 1);
 by (asm_full_simp_tac (simpset() addsimps [less_fun]) 1);
@@ -56,10 +54,10 @@
 qed "ub2ub_fun";
 
 (* ------------------------------------------------------------------------ *)
-(* Type 'a::term => 'b::pcpo is chain complete                              *)
+(* Type 'a::type => 'b::pcpo is chain complete                              *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "chain(S::nat=>('a::term => 'b::cpo)) ==> \
+Goal "chain(S::nat=>('a::type => 'b::cpo)) ==> \
 \        range(S) <<| (% x. lub(range(% i. S(i)(x))))";
 by (rtac is_lubI 1);
 by (rtac ub_rangeI 1);
@@ -78,7 +76,7 @@
 bind_thm ("thelub_fun", lub_fun RS thelubI);
 (* chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
 
-Goal "chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x";
+Goal "chain(S::nat=>('a::type => 'b::cpo)) ==> ? x. range(S) <<| x";
 by (rtac exI 1);
 by (etac lub_fun 1);
 qed "cpo_fun";
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/Fun2.thy
--- a/src/HOLCF/Fun2.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Fun2.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -2,15 +2,13 @@
     ID:         $Id$
     Author:     Franz Regensburger
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
-
-Class Instance =>::(term,po)po
 *)
 
 Fun2 = Fun1 + 
 
-(* default class is still term !*)
+(* default class is still type!*)
 
-instance fun  :: (term,po)po (refl_less_fun,antisym_less_fun,trans_less_fun)
+instance fun  :: (type, po) po (refl_less_fun,antisym_less_fun,trans_less_fun)
 
 end
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/Fun3.thy
--- a/src/HOLCF/Fun3.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Fun3.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -8,10 +8,10 @@
 
 Fun3 = Fun2 +
 
-(* default class is still term *)
+(* default class is still type *)
 
-instance fun  :: (term,cpo)cpo         (cpo_fun)
-instance fun  :: (term,pcpo)pcpo       (least_fun)
+instance fun  :: (type, cpo) cpo         (cpo_fun)
+instance fun  :: (type, pcpo)pcpo       (least_fun)
 
 end
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/IMP/Denotational.thy
--- a/src/HOLCF/IMP/Denotational.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IMP/Denotational.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -9,7 +9,7 @@
 Denotational = HOLCF + Natural +
 
 constdefs
-   dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)"
+   dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)"
   "dlift f == (LAM x. case x of UU => UU | Def(y) => f$(Discr y))"
 
 consts D :: "com => state discr -> state lift"
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/IOA/NTP/Multiset.thy
--- a/src/HOLCF/IOA/NTP/Multiset.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Multiset.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -15,7 +15,7 @@
 
 arities
 
-  multiset :: (term) term
+  multiset :: (type) type
 
 consts
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/IOA/Storage/Correctness.thy
--- a/src/HOLCF/IOA/Storage/Correctness.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/Storage/Correctness.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
 
 Correctness = SimCorrectness + Spec + Impl + 
 
-default term
+default type
 
 consts
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/IOA/meta_theory/Abstraction.thy
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -9,7 +9,7 @@
 		       
 Abstraction = LiveIOA + 
 
-default term
+default type
 
 
 consts
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOLCF/IOA/meta_theory/Automata.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -9,7 +9,7 @@
 		       
 Automata = Option + Asig + Inductive +
 
-default term
+default type
  
 types
    ('a,'s)transition       =    "'s * 'a * 's"
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/IOA/meta_theory/LiveIOA.thy
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
   
 LiveIOA = TLS + 
 
-default term
+default type
 
 types
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/IOA/meta_theory/Pred.thy
--- a/src/HOLCF/IOA/meta_theory/Pred.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
 	       
 Pred = Main +
 
-default term
+default type
 
 types
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/IOA/meta_theory/RefMappings.thy
--- a/src/HOLCF/IOA/meta_theory/RefMappings.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
 
 RefMappings = Traces  +
 
-default term
+default type
 
 consts
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -8,9 +8,9 @@
 
 Sequence = Seq + 
 
-default term
+default type
 
-types 'a Seq = ('a::term lift)seq
+types 'a Seq = ('a::type lift)seq
 
 consts
 
@@ -89,5 +89,4 @@
 (* for test purposes should be deleted FIX !! *)
 adm_all    "adm f"
 
-
-end
\ No newline at end of file
+end
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/IOA/meta_theory/Simulations.thy
--- a/src/HOLCF/IOA/meta_theory/Simulations.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Simulations.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
 
 Simulations = RefCorrectness  +
 
-default term
+default type
 
 consts
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/IOA/meta_theory/TL.thy
--- a/src/HOLCF/IOA/meta_theory/TL.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/TL.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
 	       
 TL = Pred + Sequence +  
 
-default term
+default type
 
 types
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/IOA/meta_theory/TLS.thy
--- a/src/HOLCF/IOA/meta_theory/TLS.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -9,7 +9,7 @@
 		       
 TLS = IOA + TL + 
 
-default term
+default type
 
 types
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/IOA/meta_theory/Traces.thy
--- a/src/HOLCF/IOA/meta_theory/Traces.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -9,7 +9,7 @@
 		       
 Traces = Sequence + Automata +
 
-default term
+default type
  
 types  
    ('a,'s)pairs            =    "('a * 's) Seq"
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Lift.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -4,11 +4,11 @@
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
-header {* Lifting types of class term to flat pcpo's *}
+header {* Lifting types of class type to flat pcpo's *}
 
 theory Lift = Cprod3:
 
-defaultsort "term"
+defaultsort type
 
 
 typedef 'a lift = "UNIV :: 'a option set" ..
@@ -19,12 +19,12 @@
   Def :: "'a => 'a lift"
   "Def x == Abs_lift (Some x)"
 
-instance lift :: ("term") sq_ord ..
+instance lift :: (type) sq_ord ..
 
 defs (overloaded)
   less_lift_def: "x << y == (x=y | x=Undef)"
 
-instance lift :: ("term") po
+instance lift :: (type) po
 proof
   fix x y z :: "'a lift"
   show "x << x" by (unfold less_lift_def) blast
@@ -111,7 +111,7 @@
   apply (blast intro: lub_finch1)
   done
 
-instance lift :: ("term") pcpo
+instance lift :: (type) pcpo
   apply intro_classes
    apply (erule cpo_lift)
   apply (rule least_lift)
@@ -153,7 +153,7 @@
 consts
  flift1      :: "('a => 'b::pcpo) => ('a lift -> 'b)"
  flift2      :: "('a => 'b)       => ('a lift -> 'b lift)"
- liftpair    ::"'a::term lift * 'b::term lift => ('a * 'b) lift"
+ liftpair    ::"'a::type lift * 'b::type lift => ('a * 'b) lift"
 
 defs
  flift1_def:
@@ -219,7 +219,7 @@
 
 subsection {* Lift is flat *}
 
-instance lift :: ("term") flat
+instance lift :: (type) flat
 proof
   show "ALL x y::'a lift. x << y --> x = UU | x = y"
     by (simp add: less_lift)
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Porder.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -18,8 +18,7 @@
         finite_chain :: "(nat=>'a::po)=>bool"
 
 syntax
-
-  "@LUB"	:: "(('b::term) => 'a) => 'a"	(binder "LUB " 10)
+  "@LUB"	:: "('b => 'a) => 'a"	(binder "LUB " 10)
 
 translations
 
diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/Porder0.thy
--- a/src/HOLCF/Porder0.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Porder0.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -9,7 +9,7 @@
 Porder0 = Main +
 
 	(* introduce a (syntactic) class for the constant << *)
-axclass sq_ord<term
+axclass sq_ord < type
 
 	(* characteristic constant << for po *)
 consts