renamed class "term" to "type" (actually "HOL.type");
authorwenzelm
Sat Dec 01 18:52:32 2001 +0100 (2001-12-01)
changeset 12338de0f4a63baa5
parent 12337 7c6a970f0808
child 12339 f0b62ad4e1a6
renamed class "term" to "type" (actually "HOL.type");
doc-src/AxClass/Group/Group.thy
doc-src/AxClass/Group/Product.thy
doc-src/AxClass/Group/Semigroups.thy
doc-src/AxClass/generated/Group.tex
doc-src/AxClass/generated/Product.tex
doc-src/AxClass/generated/Semigroups.tex
doc-src/TutorialI/Types/Overloading.thy
doc-src/TutorialI/Types/Overloading1.thy
doc-src/TutorialI/Types/document/Overloading.tex
doc-src/TutorialI/Types/document/Overloading1.tex
doc-src/TutorialI/tutorial.ind
src/HOL/AxClasses/Group.thy
src/HOL/AxClasses/Product.thy
src/HOL/AxClasses/Semigroups.thy
src/HOL/Divides.thy
src/HOL/Finite.thy
src/HOL/Fun.ML
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/IMP/Com.thy
src/HOL/IMP/Expr.thy
src/HOL/IMPP/Com.thy
src/HOL/Induct/Com.thy
src/HOL/Integ/Bin.ML
src/HOL/Integ/nat_simprocs.ML
src/HOL/Lattice/Lattice.thy
src/HOL/Lattice/Orders.thy
src/HOL/Library/List_Prefix.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Quotient.thy
src/HOL/MicroJava/J/Type.thy
src/HOL/MicroJava/J/Value.thy
src/HOL/MiniML/Type.thy
src/HOL/Nat.thy
src/HOL/NatDef.thy
src/HOL/Numeral.thy
src/HOL/Product_Type.thy
src/HOL/Prolog/Func.thy
src/HOL/Prolog/Test.thy
src/HOL/Prolog/Type.thy
src/HOL/Real/RealBin.ML
src/HOL/Relation_Power.thy
src/HOL/Set.thy
src/HOL/TLA/Init.thy
src/HOL/TLA/Intensional.thy
src/HOL/TLA/Memory/ProcedureInterface.thy
src/HOL/TLA/Stfun.thy
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/typedef_package.ML
src/HOL/UNITY/Comp.thy
src/HOL/UNITY/Comp/Counterc.thy
src/HOL/UNITY/Comp/PriorityAux.thy
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/GenPrefix.thy
src/HOL/UNITY/Guar.thy
src/HOL/UNITY/ListOrder.thy
src/HOL/UNITY/Simple/Reach.thy
src/HOL/W0/Type.thy
src/HOL/arith_data.ML
src/HOL/ex/MT.thy
src/HOL/ex/PER.thy
src/HOL/hologic.ML
src/HOLCF/Discrete.ML
src/HOLCF/Discrete.thy
src/HOLCF/Discrete0.ML
src/HOLCF/Discrete0.thy
src/HOLCF/Discrete1.ML
src/HOLCF/Discrete1.thy
src/HOLCF/FOCUS/Buffer.thy
src/HOLCF/FOCUS/Fstream.thy
src/HOLCF/Fun1.ML
src/HOLCF/Fun1.thy
src/HOLCF/Fun2.ML
src/HOLCF/Fun2.thy
src/HOLCF/Fun3.thy
src/HOLCF/IMP/Denotational.thy
src/HOLCF/IOA/NTP/Multiset.thy
src/HOLCF/IOA/Storage/Correctness.thy
src/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOLCF/IOA/meta_theory/Automata.thy
src/HOLCF/IOA/meta_theory/LiveIOA.thy
src/HOLCF/IOA/meta_theory/Pred.thy
src/HOLCF/IOA/meta_theory/RefMappings.thy
src/HOLCF/IOA/meta_theory/Sequence.thy
src/HOLCF/IOA/meta_theory/Simulations.thy
src/HOLCF/IOA/meta_theory/TL.thy
src/HOLCF/IOA/meta_theory/TLS.thy
src/HOLCF/IOA/meta_theory/Traces.thy
src/HOLCF/Lift.thy
src/HOLCF/Porder.thy
src/HOLCF/Porder0.thy
     1.1 --- a/doc-src/AxClass/Group/Group.thy	Sat Dec 01 18:51:46 2001 +0100
     1.2 +++ b/doc-src/AxClass/Group/Group.thy	Sat Dec 01 18:52:32 2001 +0100
     1.3 @@ -4,20 +4,20 @@
     1.4  theory Group = Main:
     1.5  
     1.6  text {*
     1.7 - \medskip\noindent The meta-level type system of Isabelle supports
     1.8 - \emph{intersections} and \emph{inclusions} of type classes. These
     1.9 - directly correspond to intersections and inclusions of type
    1.10 - predicates in a purely set theoretic sense. This is sufficient as a
    1.11 - means to describe simple hierarchies of structures.  As an
    1.12 - illustration, we use the well-known example of semigroups, monoids,
    1.13 - general groups and Abelian groups.
    1.14 +  \medskip\noindent The meta-level type system of Isabelle supports
    1.15 +  \emph{intersections} and \emph{inclusions} of type classes. These
    1.16 +  directly correspond to intersections and inclusions of type
    1.17 +  predicates in a purely set theoretic sense. This is sufficient as a
    1.18 +  means to describe simple hierarchies of structures.  As an
    1.19 +  illustration, we use the well-known example of semigroups, monoids,
    1.20 +  general groups and Abelian groups.
    1.21  *}
    1.22  
    1.23  subsection {* Monoids and Groups *}
    1.24  
    1.25  text {*
    1.26 - First we declare some polymorphic constants required later for the
    1.27 - signature parts of our structures.
    1.28 +  First we declare some polymorphic constants required later for the
    1.29 +  signature parts of our structures.
    1.30  *}
    1.31  
    1.32  consts
    1.33 @@ -26,33 +26,33 @@
    1.34    one :: 'a    ("\<unit>")
    1.35  
    1.36  text {*
    1.37 - \noindent Next we define class @{text monoid} of monoids with
    1.38 - operations @{text \<odot>} and @{text \<unit>}.  Note that multiple class
    1.39 - axioms are allowed for user convenience --- they simply represent the
    1.40 - conjunction of their respective universal closures.
    1.41 +  \noindent Next we define class @{text monoid} of monoids with
    1.42 +  operations @{text \<odot>} and @{text \<unit>}.  Note that multiple class
    1.43 +  axioms are allowed for user convenience --- they simply represent
    1.44 +  the conjunction of their respective universal closures.
    1.45  *}
    1.46  
    1.47 -axclass monoid \<subseteq> "term"
    1.48 +axclass monoid \<subseteq> type
    1.49    assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
    1.50    left_unit: "\<unit> \<odot> x = x"
    1.51    right_unit: "x \<odot> \<unit> = x"
    1.52  
    1.53  text {*
    1.54 - \noindent So class @{text monoid} contains exactly those types @{text
    1.55 - \<tau>} where @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} and @{text "\<unit> \<Colon> \<tau>"} are
    1.56 - specified appropriately, such that @{text \<odot>} is associative and
    1.57 - @{text \<unit>} is a left and right unit element for the @{text \<odot>}
    1.58 - operation.
    1.59 +  \noindent So class @{text monoid} contains exactly those types
    1.60 +  @{text \<tau>} where @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} and @{text "\<unit> \<Colon> \<tau>"}
    1.61 +  are specified appropriately, such that @{text \<odot>} is associative and
    1.62 +  @{text \<unit>} is a left and right unit element for the @{text \<odot>}
    1.63 +  operation.
    1.64  *}
    1.65  
    1.66  text {*
    1.67 - \medskip Independently of @{text monoid}, we now define a linear
    1.68 - hierarchy of semigroups, general groups and Abelian groups.  Note
    1.69 - that the names of class axioms are automatically qualified with each
    1.70 - class name, so we may re-use common names such as @{text assoc}.
    1.71 +  \medskip Independently of @{text monoid}, we now define a linear
    1.72 +  hierarchy of semigroups, general groups and Abelian groups.  Note
    1.73 +  that the names of class axioms are automatically qualified with each
    1.74 +  class name, so we may re-use common names such as @{text assoc}.
    1.75  *}
    1.76  
    1.77 -axclass semigroup \<subseteq> "term"
    1.78 +axclass semigroup \<subseteq> type
    1.79    assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
    1.80  
    1.81  axclass group \<subseteq> semigroup
    1.82 @@ -63,32 +63,32 @@
    1.83    commute: "x \<odot> y = y \<odot> x"
    1.84  
    1.85  text {*
    1.86 - \noindent Class @{text group} inherits associativity of @{text \<odot>}
    1.87 - from @{text semigroup} and adds two further group axioms. Similarly,
    1.88 - @{text agroup} is defined as the subset of @{text group} such that
    1.89 - for all of its elements @{text \<tau>}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow>
    1.90 - \<tau>"} is even commutative.
    1.91 +  \noindent Class @{text group} inherits associativity of @{text \<odot>}
    1.92 +  from @{text semigroup} and adds two further group axioms. Similarly,
    1.93 +  @{text agroup} is defined as the subset of @{text group} such that
    1.94 +  for all of its elements @{text \<tau>}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow>
    1.95 +  \<tau>"} is even commutative.
    1.96  *}
    1.97  
    1.98  
    1.99  subsection {* Abstract reasoning *}
   1.100  
   1.101  text {*
   1.102 - In a sense, axiomatic type classes may be viewed as \emph{abstract
   1.103 - theories}.  Above class definitions gives rise to abstract axioms
   1.104 - @{text assoc}, @{text left_unit}, @{text left_inverse}, @{text
   1.105 - commute}, where any of these contain a type variable @{text "'a \<Colon> c"}
   1.106 - that is restricted to types of the corresponding class @{text c}.
   1.107 - \emph{Sort constraints} like this express a logical precondition for
   1.108 - the whole formula.  For example, @{text assoc} states that for all
   1.109 - @{text \<tau>}, provided that @{text "\<tau> \<Colon> semigroup"}, the operation
   1.110 - @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is associative.
   1.111 +  In a sense, axiomatic type classes may be viewed as \emph{abstract
   1.112 +  theories}.  Above class definitions gives rise to abstract axioms
   1.113 +  @{text assoc}, @{text left_unit}, @{text left_inverse}, @{text
   1.114 +  commute}, where any of these contain a type variable @{text "'a \<Colon>
   1.115 +  c"} that is restricted to types of the corresponding class @{text
   1.116 +  c}.  \emph{Sort constraints} like this express a logical
   1.117 +  precondition for the whole formula.  For example, @{text assoc}
   1.118 +  states that for all @{text \<tau>}, provided that @{text "\<tau> \<Colon>
   1.119 +  semigroup"}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is associative.
   1.120  
   1.121 - \medskip From a technical point of view, abstract axioms are just
   1.122 - ordinary Isabelle theorems, which may be used in proofs without
   1.123 - special treatment.  Such ``abstract proofs'' usually yield new
   1.124 - ``abstract theorems''.  For example, we may now derive the following
   1.125 - well-known laws of general groups.
   1.126 +  \medskip From a technical point of view, abstract axioms are just
   1.127 +  ordinary Isabelle theorems, which may be used in proofs without
   1.128 +  special treatment.  Such ``abstract proofs'' usually yield new
   1.129 +  ``abstract theorems''.  For example, we may now derive the following
   1.130 +  well-known laws of general groups.
   1.131  *}
   1.132  
   1.133  theorem group_right_inverse: "x \<odot> x\<inv> = (\<unit>\<Colon>'a\<Colon>group)"
   1.134 @@ -113,9 +113,9 @@
   1.135  qed
   1.136  
   1.137  text {*
   1.138 - \noindent With @{text group_right_inverse} already available, @{text
   1.139 - group_right_unit}\label{thm:group-right-unit} is now established much
   1.140 - easier.
   1.141 +  \noindent With @{text group_right_inverse} already available, @{text
   1.142 +  group_right_unit}\label{thm:group-right-unit} is now established
   1.143 +  much easier.
   1.144  *}
   1.145  
   1.146  theorem group_right_unit: "x \<odot> \<unit> = (x\<Colon>'a\<Colon>group)"
   1.147 @@ -132,26 +132,26 @@
   1.148  qed
   1.149  
   1.150  text {*
   1.151 - \medskip Abstract theorems may be instantiated to only those types
   1.152 - @{text \<tau>} where the appropriate class membership @{text "\<tau> \<Colon> c"} is
   1.153 - known at Isabelle's type signature level.  Since we have @{text
   1.154 - "agroup \<subseteq> group \<subseteq> semigroup"} by definition, all theorems of @{text
   1.155 - semigroup} and @{text group} are automatically inherited by @{text
   1.156 - group} and @{text agroup}.
   1.157 +  \medskip Abstract theorems may be instantiated to only those types
   1.158 +  @{text \<tau>} where the appropriate class membership @{text "\<tau> \<Colon> c"} is
   1.159 +  known at Isabelle's type signature level.  Since we have @{text
   1.160 +  "agroup \<subseteq> group \<subseteq> semigroup"} by definition, all theorems of @{text
   1.161 +  semigroup} and @{text group} are automatically inherited by @{text
   1.162 +  group} and @{text agroup}.
   1.163  *}
   1.164  
   1.165  
   1.166  subsection {* Abstract instantiation *}
   1.167  
   1.168  text {*
   1.169 - From the definition, the @{text monoid} and @{text group} classes
   1.170 - have been independent.  Note that for monoids, @{text right_unit} had
   1.171 - to be included as an axiom, but for groups both @{text right_unit}
   1.172 - and @{text right_inverse} are derivable from the other axioms.  With
   1.173 - @{text group_right_unit} derived as a theorem of group theory (see
   1.174 - page~\pageref{thm:group-right-unit}), we may now instantiate @{text
   1.175 - "monoid \<subseteq> semigroup"} and @{text "group \<subseteq> monoid"} properly as
   1.176 - follows (cf.\ \figref{fig:monoid-group}).
   1.177 +  From the definition, the @{text monoid} and @{text group} classes
   1.178 +  have been independent.  Note that for monoids, @{text right_unit}
   1.179 +  had to be included as an axiom, but for groups both @{text
   1.180 +  right_unit} and @{text right_inverse} are derivable from the other
   1.181 +  axioms.  With @{text group_right_unit} derived as a theorem of group
   1.182 +  theory (see page~\pageref{thm:group-right-unit}), we may now
   1.183 +  instantiate @{text "monoid \<subseteq> semigroup"} and @{text "group \<subseteq>
   1.184 +  monoid"} properly as follows (cf.\ \figref{fig:monoid-group}).
   1.185  
   1.186   \begin{figure}[htbp]
   1.187     \begin{center}
   1.188 @@ -163,7 +163,7 @@
   1.189         \put(15,5){\makebox(0,0){@{text agroup}}}
   1.190         \put(15,25){\makebox(0,0){@{text group}}}
   1.191         \put(15,45){\makebox(0,0){@{text semigroup}}}
   1.192 -       \put(30,65){\makebox(0,0){@{text "term"}}} \put(50,45){\makebox(0,0){@{text monoid}}}
   1.193 +       \put(30,65){\makebox(0,0){@{text type}}} \put(50,45){\makebox(0,0){@{text monoid}}}
   1.194       \end{picture}
   1.195       \hspace{4em}
   1.196       \begin{picture}(30,90)(0,0)
   1.197 @@ -173,7 +173,7 @@
   1.198         \put(15,25){\makebox(0,0){@{text group}}}
   1.199         \put(15,45){\makebox(0,0){@{text monoid}}}
   1.200         \put(15,65){\makebox(0,0){@{text semigroup}}}
   1.201 -       \put(15,85){\makebox(0,0){@{text term}}}
   1.202 +       \put(15,85){\makebox(0,0){@{text type}}}
   1.203       \end{picture}
   1.204       \caption{Monoids and groups: according to definition, and by proof}
   1.205       \label{fig:monoid-group}
   1.206 @@ -200,34 +200,34 @@
   1.207  qed
   1.208  
   1.209  text {*
   1.210 - \medskip The $\INSTANCE$ command sets up an appropriate goal that
   1.211 - represents the class inclusion (or type arity, see
   1.212 - \secref{sec:inst-arity}) to be proven (see also
   1.213 - \cite{isabelle-isar-ref}).  The initial proof step causes
   1.214 - back-chaining of class membership statements wrt.\ the hierarchy of
   1.215 - any classes defined in the current theory; the effect is to reduce to
   1.216 - the initial statement to a number of goals that directly correspond
   1.217 - to any class axioms encountered on the path upwards through the class
   1.218 - hierarchy.
   1.219 +  \medskip The $\INSTANCE$ command sets up an appropriate goal that
   1.220 +  represents the class inclusion (or type arity, see
   1.221 +  \secref{sec:inst-arity}) to be proven (see also
   1.222 +  \cite{isabelle-isar-ref}).  The initial proof step causes
   1.223 +  back-chaining of class membership statements wrt.\ the hierarchy of
   1.224 +  any classes defined in the current theory; the effect is to reduce
   1.225 +  to the initial statement to a number of goals that directly
   1.226 +  correspond to any class axioms encountered on the path upwards
   1.227 +  through the class hierarchy.
   1.228  *}
   1.229  
   1.230  
   1.231  subsection {* Concrete instantiation \label{sec:inst-arity} *}
   1.232  
   1.233  text {*
   1.234 - So far we have covered the case of the form $\INSTANCE$~@{text
   1.235 - "c\<^sub>1 \<subseteq> c\<^sub>2"}, namely \emph{abstract instantiation} ---
   1.236 - $c@1$ is more special than @{text "c\<^sub>1"} and thus an instance
   1.237 - of @{text "c\<^sub>2"}.  Even more interesting for practical
   1.238 - applications are \emph{concrete instantiations} of axiomatic type
   1.239 - classes.  That is, certain simple schemes @{text "(\<alpha>\<^sub>1, \<dots>,
   1.240 - \<alpha>\<^sub>n) t \<Colon> c"} of class membership may be established at the
   1.241 - logical level and then transferred to Isabelle's type signature
   1.242 - level.
   1.243 +  So far we have covered the case of the form $\INSTANCE$~@{text
   1.244 +  "c\<^sub>1 \<subseteq> c\<^sub>2"}, namely \emph{abstract instantiation} ---
   1.245 +  $c@1$ is more special than @{text "c\<^sub>1"} and thus an instance
   1.246 +  of @{text "c\<^sub>2"}.  Even more interesting for practical
   1.247 +  applications are \emph{concrete instantiations} of axiomatic type
   1.248 +  classes.  That is, certain simple schemes @{text "(\<alpha>\<^sub>1, \<dots>,
   1.249 +  \<alpha>\<^sub>n) t \<Colon> c"} of class membership may be established at the
   1.250 +  logical level and then transferred to Isabelle's type signature
   1.251 +  level.
   1.252  
   1.253 - \medskip As a typical example, we show that type @{typ bool} with
   1.254 - exclusive-or as @{text \<odot>} operation, identity as @{text \<inv>}, and
   1.255 - @{term False} as @{text \<unit>} forms an Abelian group.
   1.256 +  \medskip As a typical example, we show that type @{typ bool} with
   1.257 +  exclusive-or as @{text \<odot>} operation, identity as @{text \<inv>}, and
   1.258 +  @{term False} as @{text \<unit>} forms an Abelian group.
   1.259  *}
   1.260  
   1.261  defs (overloaded)
   1.262 @@ -236,18 +236,18 @@
   1.263    unit_bool_def: "\<unit> \<equiv> False"
   1.264  
   1.265  text {*
   1.266 - \medskip It is important to note that above $\DEFS$ are just
   1.267 - overloaded meta-level constant definitions, where type classes are
   1.268 - not yet involved at all.  This form of constant definition with
   1.269 - overloading (and optional recursion over the syntactic structure of
   1.270 - simple types) are admissible as definitional extensions of plain HOL
   1.271 - \cite{Wenzel:1997:TPHOL}.  The Haskell-style type system is not
   1.272 - required for overloading.  Nevertheless, overloaded definitions are
   1.273 - best applied in the context of type classes.
   1.274 +  \medskip It is important to note that above $\DEFS$ are just
   1.275 +  overloaded meta-level constant definitions, where type classes are
   1.276 +  not yet involved at all.  This form of constant definition with
   1.277 +  overloading (and optional recursion over the syntactic structure of
   1.278 +  simple types) are admissible as definitional extensions of plain HOL
   1.279 +  \cite{Wenzel:1997:TPHOL}.  The Haskell-style type system is not
   1.280 +  required for overloading.  Nevertheless, overloaded definitions are
   1.281 +  best applied in the context of type classes.
   1.282  
   1.283 - \medskip Since we have chosen above $\DEFS$ of the generic group
   1.284 - operations on type @{typ bool} appropriately, the class membership
   1.285 - @{text "bool \<Colon> agroup"} may be now derived as follows.
   1.286 +  \medskip Since we have chosen above $\DEFS$ of the generic group
   1.287 +  operations on type @{typ bool} appropriately, the class membership
   1.288 +  @{text "bool \<Colon> agroup"} may be now derived as follows.
   1.289  *}
   1.290  
   1.291  instance bool :: agroup
   1.292 @@ -261,44 +261,44 @@
   1.293  qed
   1.294  
   1.295  text {*
   1.296 - The result of an $\INSTANCE$ statement is both expressed as a theorem
   1.297 - of Isabelle's meta-logic, and as a type arity of the type signature.
   1.298 - The latter enables type-inference system to take care of this new
   1.299 - instance automatically.
   1.300 +  The result of an $\INSTANCE$ statement is both expressed as a
   1.301 +  theorem of Isabelle's meta-logic, and as a type arity of the type
   1.302 +  signature.  The latter enables type-inference system to take care of
   1.303 +  this new instance automatically.
   1.304  
   1.305 - \medskip We could now also instantiate our group theory classes to
   1.306 - many other concrete types.  For example, @{text "int \<Colon> agroup"}
   1.307 - (e.g.\ by defining @{text \<odot>} as addition, @{text \<inv>} as negation
   1.308 - and @{text \<unit>} as zero) or @{text "list \<Colon> (term) semigroup"}
   1.309 - (e.g.\ if @{text \<odot>} is defined as list append).  Thus, the
   1.310 - characteristic constants @{text \<odot>}, @{text \<inv>}, @{text \<unit>}
   1.311 - really become overloaded, i.e.\ have different meanings on different
   1.312 - types.
   1.313 +  \medskip We could now also instantiate our group theory classes to
   1.314 +  many other concrete types.  For example, @{text "int \<Colon> agroup"}
   1.315 +  (e.g.\ by defining @{text \<odot>} as addition, @{text \<inv>} as negation
   1.316 +  and @{text \<unit>} as zero) or @{text "list \<Colon> (type) semigroup"}
   1.317 +  (e.g.\ if @{text \<odot>} is defined as list append).  Thus, the
   1.318 +  characteristic constants @{text \<odot>}, @{text \<inv>}, @{text \<unit>}
   1.319 +  really become overloaded, i.e.\ have different meanings on different
   1.320 +  types.
   1.321  *}
   1.322  
   1.323  
   1.324  subsection {* Lifting and Functors *}
   1.325  
   1.326  text {*
   1.327 - As already mentioned above, overloading in the simply-typed HOL
   1.328 - systems may include recursion over the syntactic structure of types.
   1.329 - That is, definitional equations @{text "c\<^sup>\<tau> \<equiv> t"} may also
   1.330 - contain constants of name @{text c} on the right-hand side --- if
   1.331 - these have types that are structurally simpler than @{text \<tau>}.
   1.332 +  As already mentioned above, overloading in the simply-typed HOL
   1.333 +  systems may include recursion over the syntactic structure of types.
   1.334 +  That is, definitional equations @{text "c\<^sup>\<tau> \<equiv> t"} may also
   1.335 +  contain constants of name @{text c} on the right-hand side --- if
   1.336 +  these have types that are structurally simpler than @{text \<tau>}.
   1.337  
   1.338 - This feature enables us to \emph{lift operations}, say to Cartesian
   1.339 - products, direct sums or function spaces.  Subsequently we lift
   1.340 - @{text \<odot>} component-wise to binary products @{typ "'a \<times> 'b"}.
   1.341 +  This feature enables us to \emph{lift operations}, say to Cartesian
   1.342 +  products, direct sums or function spaces.  Subsequently we lift
   1.343 +  @{text \<odot>} component-wise to binary products @{typ "'a \<times> 'b"}.
   1.344  *}
   1.345  
   1.346  defs (overloaded)
   1.347    times_prod_def: "p \<odot> q \<equiv> (fst p \<odot> fst q, snd p \<odot> snd q)"
   1.348  
   1.349  text {*
   1.350 - It is very easy to see that associativity of @{text \<odot>} on @{typ 'a}
   1.351 - and @{text \<odot>} on @{typ 'b} transfers to @{text \<odot>} on @{typ "'a \<times>
   1.352 - 'b"}.  Hence the binary type constructor @{text \<odot>} maps semigroups to
   1.353 - semigroups.  This may be established formally as follows.
   1.354 +  It is very easy to see that associativity of @{text \<odot>} on @{typ 'a}
   1.355 +  and @{text \<odot>} on @{typ 'b} transfers to @{text \<odot>} on @{typ "'a \<times>
   1.356 +  'b"}.  Hence the binary type constructor @{text \<odot>} maps semigroups
   1.357 +  to semigroups.  This may be established formally as follows.
   1.358  *}
   1.359  
   1.360  instance * :: (semigroup, semigroup) semigroup
   1.361 @@ -313,10 +313,10 @@
   1.362  qed
   1.363  
   1.364  text {*
   1.365 - Thus, if we view class instances as ``structures'', then overloaded
   1.366 - constant definitions with recursion over types indirectly provide
   1.367 - some kind of ``functors'' --- i.e.\ mappings between abstract
   1.368 - theories.
   1.369 +  Thus, if we view class instances as ``structures'', then overloaded
   1.370 +  constant definitions with recursion over types indirectly provide
   1.371 +  some kind of ``functors'' --- i.e.\ mappings between abstract
   1.372 +  theories.
   1.373  *}
   1.374  
   1.375 -end
   1.376 \ No newline at end of file
   1.377 +end
     2.1 --- a/doc-src/AxClass/Group/Product.thy	Sat Dec 01 18:51:46 2001 +0100
     2.2 +++ b/doc-src/AxClass/Group/Product.thy	Sat Dec 01 18:52:32 2001 +0100
     2.3 @@ -4,52 +4,53 @@
     2.4  theory Product = Main:
     2.5  
     2.6  text {*
     2.7 - \medskip\noindent There is still a feature of Isabelle's type system
     2.8 - left that we have not yet discussed.  When declaring polymorphic
     2.9 - constants @{text "c \<Colon> \<sigma>"}, the type variables occurring in @{text \<sigma>}
    2.10 - may be constrained by type classes (or even general sorts) in an
    2.11 - arbitrary way.  Note that by default, in Isabelle/HOL the declaration
    2.12 - @{text "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} is actually an abbreviation for @{text "\<odot>
    2.13 - \<Colon> 'a\<Colon>term \<Rightarrow> 'a \<Rightarrow> 'a"} Since class @{text "term"} is the universal
    2.14 - class of HOL, this is not really a constraint at all.
    2.15 +  \medskip\noindent There is still a feature of Isabelle's type system
    2.16 +  left that we have not yet discussed.  When declaring polymorphic
    2.17 +  constants @{text "c \<Colon> \<sigma>"}, the type variables occurring in @{text \<sigma>}
    2.18 +  may be constrained by type classes (or even general sorts) in an
    2.19 +  arbitrary way.  Note that by default, in Isabelle/HOL the
    2.20 +  declaration @{text "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} is actually an abbreviation
    2.21 +  for @{text "\<odot> \<Colon> 'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> 'a"} Since class @{text type} is the
    2.22 +  universal class of HOL, this is not really a constraint at all.
    2.23  
    2.24   The @{text product} class below provides a less degenerate example of
    2.25   syntactic type classes.
    2.26  *}
    2.27  
    2.28  axclass
    2.29 -  product \<subseteq> "term"
    2.30 +  product \<subseteq> type
    2.31  consts
    2.32    product :: "'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
    2.33  
    2.34  text {*
    2.35 - Here class @{text product} is defined as subclass of @{text term}
    2.36 - without any additional axioms.  This effects in logical equivalence
    2.37 - of @{text product} and @{text term}, as is reflected by the trivial
    2.38 - introduction rule generated for this definition.
    2.39 +  Here class @{text product} is defined as subclass of @{text type}
    2.40 +  without any additional axioms.  This effects in logical equivalence
    2.41 +  of @{text product} and @{text type}, as is reflected by the trivial
    2.42 +  introduction rule generated for this definition.
    2.43  
    2.44 - \medskip So what is the difference of declaring @{text "\<odot> \<Colon>
    2.45 - 'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"} vs.\ declaring @{text "\<odot> \<Colon> 'a\<Colon>term \<Rightarrow> 'a \<Rightarrow> 'a"}
    2.46 - anyway?  In this particular case where @{text "product \<equiv> term"}, it
    2.47 - should be obvious that both declarations are the same from the
    2.48 - logic's point of view.  It even makes the most sense to remove sort
    2.49 - constraints from constant declarations, as far as the purely logical
    2.50 - meaning is concerned \cite{Wenzel:1997:TPHOL}.
    2.51 +  \medskip So what is the difference of declaring @{text "\<odot> \<Colon>
    2.52 +  'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"} vs.\ declaring @{text "\<odot> \<Colon> 'a\<Colon>type \<Rightarrow> 'a \<Rightarrow>
    2.53 +  'a"} anyway?  In this particular case where @{text "product \<equiv>
    2.54 +  type"}, it should be obvious that both declarations are the same
    2.55 +  from the logic's point of view.  It even makes the most sense to
    2.56 +  remove sort constraints from constant declarations, as far as the
    2.57 +  purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}.
    2.58  
    2.59 - On the other hand there are syntactic differences, of course.
    2.60 - Constants @{text \<odot>} on some type @{text \<tau>} are rejected by the
    2.61 - type-checker, unless the arity @{text "\<tau> \<Colon> product"} is part of the
    2.62 - type signature.  In our example, this arity may be always added when
    2.63 - required by means of an $\INSTANCE$ with the default proof $\DDOT$.
    2.64 +  On the other hand there are syntactic differences, of course.
    2.65 +  Constants @{text \<odot>} on some type @{text \<tau>} are rejected by the
    2.66 +  type-checker, unless the arity @{text "\<tau> \<Colon> product"} is part of the
    2.67 +  type signature.  In our example, this arity may be always added when
    2.68 +  required by means of an $\INSTANCE$ with the default proof $\DDOT$.
    2.69  
    2.70 - \medskip Thus, we may observe the following discipline of using
    2.71 - syntactic classes.  Overloaded polymorphic constants have their type
    2.72 - arguments restricted to an associated (logically trivial) class
    2.73 - @{text c}.  Only immediately before \emph{specifying} these constants
    2.74 - on a certain type @{text \<tau>} do we instantiate @{text "\<tau> \<Colon> c"}.
    2.75 +  \medskip Thus, we may observe the following discipline of using
    2.76 +  syntactic classes.  Overloaded polymorphic constants have their type
    2.77 +  arguments restricted to an associated (logically trivial) class
    2.78 +  @{text c}.  Only immediately before \emph{specifying} these
    2.79 +  constants on a certain type @{text \<tau>} do we instantiate @{text "\<tau> \<Colon>
    2.80 +  c"}.
    2.81  
    2.82 - This is done for class @{text product} and type @{typ bool} as
    2.83 - follows.
    2.84 +  This is done for class @{text product} and type @{typ bool} as
    2.85 +  follows.
    2.86  *}
    2.87  
    2.88  instance bool :: product ..
    2.89 @@ -80,4 +81,4 @@
    2.90   ``providing operations'' or even ``names of functions''.
    2.91  *}
    2.92  
    2.93 -end
    2.94 \ No newline at end of file
    2.95 +end
     3.1 --- a/doc-src/AxClass/Group/Semigroups.thy	Sat Dec 01 18:51:46 2001 +0100
     3.2 +++ b/doc-src/AxClass/Group/Semigroups.thy	Sat Dec 01 18:52:32 2001 +0100
     3.3 @@ -4,50 +4,51 @@
     3.4  theory Semigroups = Main:
     3.5  
     3.6  text {*
     3.7 - \medskip\noindent An axiomatic type class is simply a class of types
     3.8 - that all meet certain properties, which are also called \emph{class
     3.9 - axioms}. Thus, type classes may be also understood as type predicates
    3.10 - --- i.e.\ abstractions over a single type argument @{typ 'a}.  Class
    3.11 - axioms typically contain polymorphic constants that depend on this
    3.12 - type @{typ 'a}.  These \emph{characteristic constants} behave like
    3.13 - operations associated with the ``carrier'' type @{typ 'a}.
    3.14 +  \medskip\noindent An axiomatic type class is simply a class of types
    3.15 +  that all meet certain properties, which are also called \emph{class
    3.16 +  axioms}. Thus, type classes may be also understood as type
    3.17 +  predicates --- i.e.\ abstractions over a single type argument @{typ
    3.18 +  'a}.  Class axioms typically contain polymorphic constants that
    3.19 +  depend on this type @{typ 'a}.  These \emph{characteristic
    3.20 +  constants} behave like operations associated with the ``carrier''
    3.21 +  type @{typ 'a}.
    3.22  
    3.23 - We illustrate these basic concepts by the following formulation of
    3.24 - semigroups.
    3.25 +  We illustrate these basic concepts by the following formulation of
    3.26 +  semigroups.
    3.27  *}
    3.28  
    3.29  consts
    3.30    times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
    3.31 -axclass semigroup \<subseteq> "term"
    3.32 +axclass semigroup \<subseteq> type
    3.33    assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
    3.34  
    3.35  text {*
    3.36 - \noindent Above we have first declared a polymorphic constant @{text
    3.37 - "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} and then defined the class @{text semigroup} of
    3.38 - all types @{text \<tau>} such that @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is indeed an
    3.39 - associative operator.  The @{text assoc} axiom contains exactly one
    3.40 - type variable, which is invisible in the above presentation, though.
    3.41 - Also note that free term variables (like @{term x}, @{term y}, @{term
    3.42 - z}) are allowed for user convenience --- conceptually all of these
    3.43 - are bound by outermost universal quantifiers.
    3.44 +  \noindent Above we have first declared a polymorphic constant @{text
    3.45 +  "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} and then defined the class @{text semigroup} of
    3.46 +  all types @{text \<tau>} such that @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is indeed an
    3.47 +  associative operator.  The @{text assoc} axiom contains exactly one
    3.48 +  type variable, which is invisible in the above presentation, though.
    3.49 +  Also note that free term variables (like @{term x}, @{term y},
    3.50 +  @{term z}) are allowed for user convenience --- conceptually all of
    3.51 +  these are bound by outermost universal quantifiers.
    3.52  
    3.53 - \medskip In general, type classes may be used to describe
    3.54 - \emph{structures} with exactly one carrier @{typ 'a} and a fixed
    3.55 - \emph{signature}.  Different signatures require different classes.
    3.56 - Below, class @{text plus_semigroup} represents semigroups 
    3.57 - @{text "(\<tau>, \<oplus>\<^sup>\<tau>)"}, while the original @{text semigroup} would
    3.58 - correspond to semigroups of the form @{text "(\<tau>, \<odot>\<^sup>\<tau>)"}.
    3.59 +  \medskip In general, type classes may be used to describe
    3.60 +  \emph{structures} with exactly one carrier @{typ 'a} and a fixed
    3.61 +  \emph{signature}.  Different signatures require different classes.
    3.62 +  Below, class @{text plus_semigroup} represents semigroups @{text
    3.63 +  "(\<tau>, \<oplus>\<^sup>\<tau>)"}, while the original @{text semigroup} would
    3.64 +  correspond to semigroups of the form @{text "(\<tau>, \<odot>\<^sup>\<tau>)"}.
    3.65  *}
    3.66  
    3.67  consts
    3.68    plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<oplus>" 70)
    3.69 -axclass plus_semigroup \<subseteq> "term"
    3.70 +axclass plus_semigroup \<subseteq> type
    3.71    assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
    3.72  
    3.73  text {*
    3.74 - \noindent Even if classes @{text plus_semigroup} and @{text
    3.75 - semigroup} both represent semigroups in a sense, they are certainly
    3.76 - not quite the same.
    3.77 +  \noindent Even if classes @{text plus_semigroup} and @{text
    3.78 +  semigroup} both represent semigroups in a sense, they are certainly
    3.79 +  not quite the same.
    3.80  *}
    3.81  
    3.82 -end
    3.83 \ No newline at end of file
    3.84 +end
     4.1 --- a/doc-src/AxClass/generated/Group.tex	Sat Dec 01 18:51:46 2001 +0100
     4.2 +++ b/doc-src/AxClass/generated/Group.tex	Sat Dec 01 18:52:32 2001 +0100
     4.3 @@ -9,12 +9,12 @@
     4.4  %
     4.5  \begin{isamarkuptext}%
     4.6  \medskip\noindent The meta-level type system of Isabelle supports
     4.7 - \emph{intersections} and \emph{inclusions} of type classes. These
     4.8 - directly correspond to intersections and inclusions of type
     4.9 - predicates in a purely set theoretic sense. This is sufficient as a
    4.10 - means to describe simple hierarchies of structures.  As an
    4.11 - illustration, we use the well-known example of semigroups, monoids,
    4.12 - general groups and Abelian groups.%
    4.13 +  \emph{intersections} and \emph{inclusions} of type classes. These
    4.14 +  directly correspond to intersections and inclusions of type
    4.15 +  predicates in a purely set theoretic sense. This is sufficient as a
    4.16 +  means to describe simple hierarchies of structures.  As an
    4.17 +  illustration, we use the well-known example of semigroups, monoids,
    4.18 +  general groups and Abelian groups.%
    4.19  \end{isamarkuptext}%
    4.20  \isamarkuptrue%
    4.21  %
    4.22 @@ -24,7 +24,7 @@
    4.23  %
    4.24  \begin{isamarkuptext}%
    4.25  First we declare some polymorphic constants required later for the
    4.26 - signature parts of our structures.%
    4.27 +  signature parts of our structures.%
    4.28  \end{isamarkuptext}%
    4.29  \isamarkuptrue%
    4.30  \isacommand{consts}\isanewline
    4.31 @@ -34,32 +34,33 @@
    4.32  %
    4.33  \begin{isamarkuptext}%
    4.34  \noindent Next we define class \isa{monoid} of monoids with
    4.35 - operations \isa{{\isasymodot}} and \isa{{\isasymunit}}.  Note that multiple class
    4.36 - axioms are allowed for user convenience --- they simply represent the
    4.37 - conjunction of their respective universal closures.%
    4.38 +  operations \isa{{\isasymodot}} and \isa{{\isasymunit}}.  Note that multiple class
    4.39 +  axioms are allowed for user convenience --- they simply represent
    4.40 +  the conjunction of their respective universal closures.%
    4.41  \end{isamarkuptext}%
    4.42  \isamarkuptrue%
    4.43 -\isacommand{axclass}\ monoid\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
    4.44 +\isacommand{axclass}\ monoid\ {\isasymsubseteq}\ type\isanewline
    4.45  \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
    4.46  \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
    4.47  \ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse%
    4.48  %
    4.49  \begin{isamarkuptext}%
    4.50 -\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
    4.51 - specified appropriately, such that \isa{{\isasymodot}} is associative and
    4.52 - \isa{{\isasymunit}} is a left and right unit element for the \isa{{\isasymodot}}
    4.53 - operation.%
    4.54 +\noindent So class \isa{monoid} contains exactly those types
    4.55 +  \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymunit}\ {\isasymColon}\ {\isasymtau}}
    4.56 +  are specified appropriately, such that \isa{{\isasymodot}} is associative and
    4.57 +  \isa{{\isasymunit}} is a left and right unit element for the \isa{{\isasymodot}}
    4.58 +  operation.%
    4.59  \end{isamarkuptext}%
    4.60  \isamarkuptrue%
    4.61  %
    4.62  \begin{isamarkuptext}%
    4.63  \medskip Independently of \isa{monoid}, we now define a linear
    4.64 - hierarchy of semigroups, general groups and Abelian groups.  Note
    4.65 - that the names of class axioms are automatically qualified with each
    4.66 - class name, so we may re-use common names such as \isa{assoc}.%
    4.67 +  hierarchy of semigroups, general groups and Abelian groups.  Note
    4.68 +  that the names of class axioms are automatically qualified with each
    4.69 +  class name, so we may re-use common names such as \isa{assoc}.%
    4.70  \end{isamarkuptext}%
    4.71  \isamarkuptrue%
    4.72 -\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
    4.73 +\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ type\isanewline
    4.74  \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
    4.75  \isanewline
    4.76  \isamarkupfalse%
    4.77 @@ -73,9 +74,9 @@
    4.78  %
    4.79  \begin{isamarkuptext}%
    4.80  \noindent Class \isa{group} inherits associativity of \isa{{\isasymodot}}
    4.81 - from \isa{semigroup} and adds two further group axioms. Similarly,
    4.82 - \isa{agroup} is defined as the subset of \isa{group} such that
    4.83 - for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is even commutative.%
    4.84 +  from \isa{semigroup} and adds two further group axioms. Similarly,
    4.85 +  \isa{agroup} is defined as the subset of \isa{group} such that
    4.86 +  for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is even commutative.%
    4.87  \end{isamarkuptext}%
    4.88  \isamarkuptrue%
    4.89  %
    4.90 @@ -85,19 +86,16 @@
    4.91  %
    4.92  \begin{isamarkuptext}%
    4.93  In a sense, axiomatic type classes may be viewed as \emph{abstract
    4.94 - theories}.  Above class definitions gives rise to abstract axioms
    4.95 - \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}
    4.96 - that is restricted to types of the corresponding class \isa{c}.
    4.97 - \emph{Sort constraints} like this express a logical precondition for
    4.98 - the whole formula.  For example, \isa{assoc} states that for all
    4.99 - \isa{{\isasymtau}}, provided that \isa{{\isasymtau}\ {\isasymColon}\ semigroup}, the operation
   4.100 - \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is associative.
   4.101 +  theories}.  Above class definitions gives rise to abstract axioms
   4.102 +  \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
   4.103 +  precondition for the whole formula.  For example, \isa{assoc}
   4.104 +  states that for all \isa{{\isasymtau}}, provided that \isa{{\isasymtau}\ {\isasymColon}\ semigroup}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is associative.
   4.105  
   4.106 - \medskip From a technical point of view, abstract axioms are just
   4.107 - ordinary Isabelle theorems, which may be used in proofs without
   4.108 - special treatment.  Such ``abstract proofs'' usually yield new
   4.109 - ``abstract theorems''.  For example, we may now derive the following
   4.110 - well-known laws of general groups.%
   4.111 +  \medskip From a technical point of view, abstract axioms are just
   4.112 +  ordinary Isabelle theorems, which may be used in proofs without
   4.113 +  special treatment.  Such ``abstract proofs'' usually yield new
   4.114 +  ``abstract theorems''.  For example, we may now derive the following
   4.115 +  well-known laws of general groups.%
   4.116  \end{isamarkuptext}%
   4.117  \isamarkuptrue%
   4.118  \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymunit}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
   4.119 @@ -150,8 +148,8 @@
   4.120  \isacommand{qed}\isamarkupfalse%
   4.121  %
   4.122  \begin{isamarkuptext}%
   4.123 -\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
   4.124 - easier.%
   4.125 +\noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established
   4.126 +  much easier.%
   4.127  \end{isamarkuptext}%
   4.128  \isamarkuptrue%
   4.129  \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
   4.130 @@ -185,8 +183,8 @@
   4.131  %
   4.132  \begin{isamarkuptext}%
   4.133  \medskip Abstract theorems may be instantiated to only those types
   4.134 - \isa{{\isasymtau}} where the appropriate class membership \isa{{\isasymtau}\ {\isasymColon}\ c} is
   4.135 - 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}.%
   4.136 +  \isa{{\isasymtau}} where the appropriate class membership \isa{{\isasymtau}\ {\isasymColon}\ c} is
   4.137 +  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}.%
   4.138  \end{isamarkuptext}%
   4.139  \isamarkuptrue%
   4.140  %
   4.141 @@ -196,12 +194,11 @@
   4.142  %
   4.143  \begin{isamarkuptext}%
   4.144  From the definition, the \isa{monoid} and \isa{group} classes
   4.145 - have been independent.  Note that for monoids, \isa{right{\isacharunderscore}unit} had
   4.146 - to be included as an axiom, but for groups both \isa{right{\isacharunderscore}unit}
   4.147 - and \isa{right{\isacharunderscore}inverse} are derivable from the other axioms.  With
   4.148 - \isa{group{\isacharunderscore}right{\isacharunderscore}unit} derived as a theorem of group theory (see
   4.149 - page~\pageref{thm:group-right-unit}), we may now instantiate \isa{monoid\ {\isasymsubseteq}\ semigroup} and \isa{group\ {\isasymsubseteq}\ monoid} properly as
   4.150 - follows (cf.\ \figref{fig:monoid-group}).
   4.151 +  have been independent.  Note that for monoids, \isa{right{\isacharunderscore}unit}
   4.152 +  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
   4.153 +  axioms.  With \isa{group{\isacharunderscore}right{\isacharunderscore}unit} derived as a theorem of group
   4.154 +  theory (see page~\pageref{thm:group-right-unit}), we may now
   4.155 +  instantiate \isa{monoid\ {\isasymsubseteq}\ semigroup} and \isa{group\ {\isasymsubseteq}\ monoid} properly as follows (cf.\ \figref{fig:monoid-group}).
   4.156  
   4.157   \begin{figure}[htbp]
   4.158     \begin{center}
   4.159 @@ -213,7 +210,7 @@
   4.160         \put(15,5){\makebox(0,0){\isa{agroup}}}
   4.161         \put(15,25){\makebox(0,0){\isa{group}}}
   4.162         \put(15,45){\makebox(0,0){\isa{semigroup}}}
   4.163 -       \put(30,65){\makebox(0,0){\isa{term}}} \put(50,45){\makebox(0,0){\isa{monoid}}}
   4.164 +       \put(30,65){\makebox(0,0){\isa{type}}} \put(50,45){\makebox(0,0){\isa{monoid}}}
   4.165       \end{picture}
   4.166       \hspace{4em}
   4.167       \begin{picture}(30,90)(0,0)
   4.168 @@ -223,7 +220,7 @@
   4.169         \put(15,25){\makebox(0,0){\isa{group}}}
   4.170         \put(15,45){\makebox(0,0){\isa{monoid}}}
   4.171         \put(15,65){\makebox(0,0){\isa{semigroup}}}
   4.172 -       \put(15,85){\makebox(0,0){\isa{term}}}
   4.173 +       \put(15,85){\makebox(0,0){\isa{type}}}
   4.174       \end{picture}
   4.175       \caption{Monoids and groups: according to definition, and by proof}
   4.176       \label{fig:monoid-group}
   4.177 @@ -266,14 +263,14 @@
   4.178  %
   4.179  \begin{isamarkuptext}%
   4.180  \medskip The $\INSTANCE$ command sets up an appropriate goal that
   4.181 - represents the class inclusion (or type arity, see
   4.182 - \secref{sec:inst-arity}) to be proven (see also
   4.183 - \cite{isabelle-isar-ref}).  The initial proof step causes
   4.184 - back-chaining of class membership statements wrt.\ the hierarchy of
   4.185 - any classes defined in the current theory; the effect is to reduce to
   4.186 - the initial statement to a number of goals that directly correspond
   4.187 - to any class axioms encountered on the path upwards through the class
   4.188 - hierarchy.%
   4.189 +  represents the class inclusion (or type arity, see
   4.190 +  \secref{sec:inst-arity}) to be proven (see also
   4.191 +  \cite{isabelle-isar-ref}).  The initial proof step causes
   4.192 +  back-chaining of class membership statements wrt.\ the hierarchy of
   4.193 +  any classes defined in the current theory; the effect is to reduce
   4.194 +  to the initial statement to a number of goals that directly
   4.195 +  correspond to any class axioms encountered on the path upwards
   4.196 +  through the class hierarchy.%
   4.197  \end{isamarkuptext}%
   4.198  \isamarkuptrue%
   4.199  %
   4.200 @@ -283,16 +280,16 @@
   4.201  %
   4.202  \begin{isamarkuptext}%
   4.203  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} ---
   4.204 - $c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance
   4.205 - of \isa{c\isactrlsub {\isadigit{2}}}.  Even more interesting for practical
   4.206 - applications are \emph{concrete instantiations} of axiomatic type
   4.207 - 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
   4.208 - logical level and then transferred to Isabelle's type signature
   4.209 - level.
   4.210 +  $c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance
   4.211 +  of \isa{c\isactrlsub {\isadigit{2}}}.  Even more interesting for practical
   4.212 +  applications are \emph{concrete instantiations} of axiomatic type
   4.213 +  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
   4.214 +  logical level and then transferred to Isabelle's type signature
   4.215 +  level.
   4.216  
   4.217 - \medskip As a typical example, we show that type \isa{bool} with
   4.218 - exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and
   4.219 - \isa{False} as \isa{{\isasymunit}} forms an Abelian group.%
   4.220 +  \medskip As a typical example, we show that type \isa{bool} with
   4.221 +  exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and
   4.222 +  \isa{False} as \isa{{\isasymunit}} forms an Abelian group.%
   4.223  \end{isamarkuptext}%
   4.224  \isamarkuptrue%
   4.225  \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
   4.226 @@ -302,17 +299,17 @@
   4.227  %
   4.228  \begin{isamarkuptext}%
   4.229  \medskip It is important to note that above $\DEFS$ are just
   4.230 - overloaded meta-level constant definitions, where type classes are
   4.231 - not yet involved at all.  This form of constant definition with
   4.232 - overloading (and optional recursion over the syntactic structure of
   4.233 - simple types) are admissible as definitional extensions of plain HOL
   4.234 - \cite{Wenzel:1997:TPHOL}.  The Haskell-style type system is not
   4.235 - required for overloading.  Nevertheless, overloaded definitions are
   4.236 - best applied in the context of type classes.
   4.237 +  overloaded meta-level constant definitions, where type classes are
   4.238 +  not yet involved at all.  This form of constant definition with
   4.239 +  overloading (and optional recursion over the syntactic structure of
   4.240 +  simple types) are admissible as definitional extensions of plain HOL
   4.241 +  \cite{Wenzel:1997:TPHOL}.  The Haskell-style type system is not
   4.242 +  required for overloading.  Nevertheless, overloaded definitions are
   4.243 +  best applied in the context of type classes.
   4.244  
   4.245 - \medskip Since we have chosen above $\DEFS$ of the generic group
   4.246 - operations on type \isa{bool} appropriately, the class membership
   4.247 - \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.%
   4.248 +  \medskip Since we have chosen above $\DEFS$ of the generic group
   4.249 +  operations on type \isa{bool} appropriately, the class membership
   4.250 +  \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.%
   4.251  \end{isamarkuptext}%
   4.252  \isamarkuptrue%
   4.253  \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline
   4.254 @@ -337,19 +334,19 @@
   4.255  \isacommand{qed}\isamarkupfalse%
   4.256  %
   4.257  \begin{isamarkuptext}%
   4.258 -The result of an $\INSTANCE$ statement is both expressed as a theorem
   4.259 - of Isabelle's meta-logic, and as a type arity of the type signature.
   4.260 - The latter enables type-inference system to take care of this new
   4.261 - instance automatically.
   4.262 +The result of an $\INSTANCE$ statement is both expressed as a
   4.263 +  theorem of Isabelle's meta-logic, and as a type arity of the type
   4.264 +  signature.  The latter enables type-inference system to take care of
   4.265 +  this new instance automatically.
   4.266  
   4.267 - \medskip We could now also instantiate our group theory classes to
   4.268 - many other concrete types.  For example, \isa{int\ {\isasymColon}\ agroup}
   4.269 - (e.g.\ by defining \isa{{\isasymodot}} as addition, \isa{{\isasyminv}} as negation
   4.270 - and \isa{{\isasymunit}} as zero) or \isa{list\ {\isasymColon}\ {\isacharparenleft}term{\isacharparenright}\ semigroup}
   4.271 - (e.g.\ if \isa{{\isasymodot}} is defined as list append).  Thus, the
   4.272 - characteristic constants \isa{{\isasymodot}}, \isa{{\isasyminv}}, \isa{{\isasymunit}}
   4.273 - really become overloaded, i.e.\ have different meanings on different
   4.274 - types.%
   4.275 +  \medskip We could now also instantiate our group theory classes to
   4.276 +  many other concrete types.  For example, \isa{int\ {\isasymColon}\ agroup}
   4.277 +  (e.g.\ by defining \isa{{\isasymodot}} as addition, \isa{{\isasyminv}} as negation
   4.278 +  and \isa{{\isasymunit}} as zero) or \isa{list\ {\isasymColon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup}
   4.279 +  (e.g.\ if \isa{{\isasymodot}} is defined as list append).  Thus, the
   4.280 +  characteristic constants \isa{{\isasymodot}}, \isa{{\isasyminv}}, \isa{{\isasymunit}}
   4.281 +  really become overloaded, i.e.\ have different meanings on different
   4.282 +  types.%
   4.283  \end{isamarkuptext}%
   4.284  \isamarkuptrue%
   4.285  %
   4.286 @@ -359,14 +356,14 @@
   4.287  %
   4.288  \begin{isamarkuptext}%
   4.289  As already mentioned above, overloading in the simply-typed HOL
   4.290 - systems may include recursion over the syntactic structure of types.
   4.291 - That is, definitional equations \isa{c\isactrlsup {\isasymtau}\ {\isasymequiv}\ t} may also
   4.292 - contain constants of name \isa{c} on the right-hand side --- if
   4.293 - these have types that are structurally simpler than \isa{{\isasymtau}}.
   4.294 +  systems may include recursion over the syntactic structure of types.
   4.295 +  That is, definitional equations \isa{c\isactrlsup {\isasymtau}\ {\isasymequiv}\ t} may also
   4.296 +  contain constants of name \isa{c} on the right-hand side --- if
   4.297 +  these have types that are structurally simpler than \isa{{\isasymtau}}.
   4.298  
   4.299 - This feature enables us to \emph{lift operations}, say to Cartesian
   4.300 - products, direct sums or function spaces.  Subsequently we lift
   4.301 - \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.%
   4.302 +  This feature enables us to \emph{lift operations}, say to Cartesian
   4.303 +  products, direct sums or function spaces.  Subsequently we lift
   4.304 +  \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.%
   4.305  \end{isamarkuptext}%
   4.306  \isamarkuptrue%
   4.307  \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
   4.308 @@ -374,8 +371,8 @@
   4.309  %
   4.310  \begin{isamarkuptext}%
   4.311  It is very easy to see that associativity of \isa{{\isasymodot}} on \isa{{\isacharprime}a}
   4.312 - 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
   4.313 - semigroups.  This may be established formally as follows.%
   4.314 +  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
   4.315 +  to semigroups.  This may be established formally as follows.%
   4.316  \end{isamarkuptext}%
   4.317  \isamarkuptrue%
   4.318  \isacommand{instance}\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
   4.319 @@ -396,12 +393,13 @@
   4.320  %
   4.321  \begin{isamarkuptext}%
   4.322  Thus, if we view class instances as ``structures'', then overloaded
   4.323 - constant definitions with recursion over types indirectly provide
   4.324 - some kind of ``functors'' --- i.e.\ mappings between abstract
   4.325 - theories.%
   4.326 +  constant definitions with recursion over types indirectly provide
   4.327 +  some kind of ``functors'' --- i.e.\ mappings between abstract
   4.328 +  theories.%
   4.329  \end{isamarkuptext}%
   4.330  \isamarkuptrue%
   4.331 -\isacommand{end}\isamarkupfalse%
   4.332 +\isacommand{end}\isanewline
   4.333 +\isamarkupfalse%
   4.334  \end{isabellebody}%
   4.335  %%% Local Variables:
   4.336  %%% mode: latex
     5.1 --- a/doc-src/AxClass/generated/Product.tex	Sat Dec 01 18:51:46 2001 +0100
     5.2 +++ b/doc-src/AxClass/generated/Product.tex	Sat Dec 01 18:52:32 2001 +0100
     5.3 @@ -9,50 +9,49 @@
     5.4  %
     5.5  \begin{isamarkuptext}%
     5.6  \medskip\noindent There is still a feature of Isabelle's type system
     5.7 - left that we have not yet discussed.  When declaring polymorphic
     5.8 - constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}}
     5.9 - may be constrained by type classes (or even general sorts) in an
    5.10 - arbitrary way.  Note that by default, in Isabelle/HOL the declaration
    5.11 - \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
    5.12 - class of HOL, this is not really a constraint at all.
    5.13 +  left that we have not yet discussed.  When declaring polymorphic
    5.14 +  constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}}
    5.15 +  may be constrained by type classes (or even general sorts) in an
    5.16 +  arbitrary way.  Note that by default, in Isabelle/HOL the
    5.17 +  declaration \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} is actually an abbreviation
    5.18 +  for \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}type\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} Since class \isa{type} is the
    5.19 +  universal class of HOL, this is not really a constraint at all.
    5.20  
    5.21   The \isa{product} class below provides a less degenerate example of
    5.22   syntactic type classes.%
    5.23  \end{isamarkuptext}%
    5.24  \isamarkuptrue%
    5.25  \isacommand{axclass}\isanewline
    5.26 -\ \ product\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
    5.27 +\ \ product\ {\isasymsubseteq}\ type\isanewline
    5.28  \isamarkupfalse%
    5.29  \isacommand{consts}\isanewline
    5.30  \ \ 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%
    5.31  %
    5.32  \begin{isamarkuptext}%
    5.33 -Here class \isa{product} is defined as subclass of \isa{term}
    5.34 - without any additional axioms.  This effects in logical equivalence
    5.35 - of \isa{product} and \isa{term}, as is reflected by the trivial
    5.36 - introduction rule generated for this definition.
    5.37 +Here class \isa{product} is defined as subclass of \isa{type}
    5.38 +  without any additional axioms.  This effects in logical equivalence
    5.39 +  of \isa{product} and \isa{type}, as is reflected by the trivial
    5.40 +  introduction rule generated for this definition.
    5.41  
    5.42 - \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}
    5.43 - anyway?  In this particular case where \isa{product\ {\isasymequiv}\ term}, it
    5.44 - should be obvious that both declarations are the same from the
    5.45 - logic's point of view.  It even makes the most sense to remove sort
    5.46 - constraints from constant declarations, as far as the purely logical
    5.47 - meaning is concerned \cite{Wenzel:1997:TPHOL}.
    5.48 +  \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
    5.49 +  from the logic's point of view.  It even makes the most sense to
    5.50 +  remove sort constraints from constant declarations, as far as the
    5.51 +  purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}.
    5.52  
    5.53 - On the other hand there are syntactic differences, of course.
    5.54 - Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the
    5.55 - type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the
    5.56 - type signature.  In our example, this arity may be always added when
    5.57 - required by means of an $\INSTANCE$ with the default proof $\DDOT$.
    5.58 +  On the other hand there are syntactic differences, of course.
    5.59 +  Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the
    5.60 +  type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the
    5.61 +  type signature.  In our example, this arity may be always added when
    5.62 +  required by means of an $\INSTANCE$ with the default proof $\DDOT$.
    5.63  
    5.64 - \medskip Thus, we may observe the following discipline of using
    5.65 - syntactic classes.  Overloaded polymorphic constants have their type
    5.66 - arguments restricted to an associated (logically trivial) class
    5.67 - \isa{c}.  Only immediately before \emph{specifying} these constants
    5.68 - on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}.
    5.69 +  \medskip Thus, we may observe the following discipline of using
    5.70 +  syntactic classes.  Overloaded polymorphic constants have their type
    5.71 +  arguments restricted to an associated (logically trivial) class
    5.72 +  \isa{c}.  Only immediately before \emph{specifying} these
    5.73 +  constants on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}.
    5.74  
    5.75 - This is done for class \isa{product} and type \isa{bool} as
    5.76 - follows.%
    5.77 +  This is done for class \isa{product} and type \isa{bool} as
    5.78 +  follows.%
    5.79  \end{isamarkuptext}%
    5.80  \isamarkuptrue%
    5.81  \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product\ \isamarkupfalse%
    5.82 @@ -85,7 +84,8 @@
    5.83   ``providing operations'' or even ``names of functions''.%
    5.84  \end{isamarkuptext}%
    5.85  \isamarkuptrue%
    5.86 -\isacommand{end}\isamarkupfalse%
    5.87 +\isacommand{end}\isanewline
    5.88 +\isamarkupfalse%
    5.89  \end{isabellebody}%
    5.90  %%% Local Variables:
    5.91  %%% mode: latex
     6.1 --- a/doc-src/AxClass/generated/Semigroups.tex	Sat Dec 01 18:51:46 2001 +0100
     6.2 +++ b/doc-src/AxClass/generated/Semigroups.tex	Sat Dec 01 18:52:32 2001 +0100
     6.3 @@ -9,51 +9,52 @@
     6.4  %
     6.5  \begin{isamarkuptext}%
     6.6  \medskip\noindent An axiomatic type class is simply a class of types
     6.7 - that all meet certain properties, which are also called \emph{class
     6.8 - axioms}. Thus, type classes may be also understood as type predicates
     6.9 - --- i.e.\ abstractions over a single type argument \isa{{\isacharprime}a}.  Class
    6.10 - axioms typically contain polymorphic constants that depend on this
    6.11 - type \isa{{\isacharprime}a}.  These \emph{characteristic constants} behave like
    6.12 - operations associated with the ``carrier'' type \isa{{\isacharprime}a}.
    6.13 +  that all meet certain properties, which are also called \emph{class
    6.14 +  axioms}. Thus, type classes may be also understood as type
    6.15 +  predicates --- i.e.\ abstractions over a single type argument \isa{{\isacharprime}a}.  Class axioms typically contain polymorphic constants that
    6.16 +  depend on this type \isa{{\isacharprime}a}.  These \emph{characteristic
    6.17 +  constants} behave like operations associated with the ``carrier''
    6.18 +  type \isa{{\isacharprime}a}.
    6.19  
    6.20 - We illustrate these basic concepts by the following formulation of
    6.21 - semigroups.%
    6.22 +  We illustrate these basic concepts by the following formulation of
    6.23 +  semigroups.%
    6.24  \end{isamarkuptext}%
    6.25  \isamarkuptrue%
    6.26  \isacommand{consts}\isanewline
    6.27  \ \ 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
    6.28  \isamarkupfalse%
    6.29 -\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
    6.30 +\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ type\isanewline
    6.31  \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
    6.32  %
    6.33  \begin{isamarkuptext}%
    6.34  \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
    6.35 - all types \isa{{\isasymtau}} such that \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is indeed an
    6.36 - associative operator.  The \isa{assoc} axiom contains exactly one
    6.37 - type variable, which is invisible in the above presentation, though.
    6.38 - Also note that free term variables (like \isa{x}, \isa{y}, \isa{z}) are allowed for user convenience --- conceptually all of these
    6.39 - are bound by outermost universal quantifiers.
    6.40 +  all types \isa{{\isasymtau}} such that \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is indeed an
    6.41 +  associative operator.  The \isa{assoc} axiom contains exactly one
    6.42 +  type variable, which is invisible in the above presentation, though.
    6.43 +  Also note that free term variables (like \isa{x}, \isa{y},
    6.44 +  \isa{z}) are allowed for user convenience --- conceptually all of
    6.45 +  these are bound by outermost universal quantifiers.
    6.46  
    6.47 - \medskip In general, type classes may be used to describe
    6.48 - \emph{structures} with exactly one carrier \isa{{\isacharprime}a} and a fixed
    6.49 - \emph{signature}.  Different signatures require different classes.
    6.50 - Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups 
    6.51 - \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}\isactrlsup {\isasymtau}{\isacharparenright}}, while the original \isa{semigroup} would
    6.52 - correspond to semigroups of the form \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}\isactrlsup {\isasymtau}{\isacharparenright}}.%
    6.53 +  \medskip In general, type classes may be used to describe
    6.54 +  \emph{structures} with exactly one carrier \isa{{\isacharprime}a} and a fixed
    6.55 +  \emph{signature}.  Different signatures require different classes.
    6.56 +  Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}\isactrlsup {\isasymtau}{\isacharparenright}}, while the original \isa{semigroup} would
    6.57 +  correspond to semigroups of the form \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}\isactrlsup {\isasymtau}{\isacharparenright}}.%
    6.58  \end{isamarkuptext}%
    6.59  \isamarkuptrue%
    6.60  \isacommand{consts}\isanewline
    6.61  \ \ 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
    6.62  \isamarkupfalse%
    6.63 -\isacommand{axclass}\ plus{\isacharunderscore}semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
    6.64 +\isacommand{axclass}\ plus{\isacharunderscore}semigroup\ {\isasymsubseteq}\ type\isanewline
    6.65  \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
    6.66  %
    6.67  \begin{isamarkuptext}%
    6.68  \noindent Even if classes \isa{plus{\isacharunderscore}semigroup} and \isa{semigroup} both represent semigroups in a sense, they are certainly
    6.69 - not quite the same.%
    6.70 +  not quite the same.%
    6.71  \end{isamarkuptext}%
    6.72  \isamarkuptrue%
    6.73 -\isacommand{end}\isamarkupfalse%
    6.74 +\isacommand{end}\isanewline
    6.75 +\isamarkupfalse%
    6.76  \end{isabellebody}%
    6.77  %%% Local Variables:
    6.78  %%% mode: latex
     7.1 --- a/doc-src/TutorialI/Types/Overloading.thy	Sat Dec 01 18:51:46 2001 +0100
     7.2 +++ b/doc-src/TutorialI/Types/Overloading.thy	Sat Dec 01 18:52:32 2001 +0100
     7.3 @@ -1,13 +1,13 @@
     7.4  (*<*)theory Overloading = Overloading1:(*>*)
     7.5 -instance list :: ("term")ordrel
     7.6 +instance list :: (type)ordrel
     7.7  by intro_classes
     7.8  
     7.9  text{*\noindent
    7.10  This \isacommand{instance} declaration can be read like the declaration of
    7.11  a function on types.  The constructor @{text list} maps types of class @{text
    7.12 -term} (all HOL types), to types of class @{text ordrel};
    7.13 +type} (all HOL types), to types of class @{text ordrel};
    7.14  in other words,
    7.15 -if @{text"ty :: term"} then @{text"ty list :: ordrel"}.
    7.16 +if @{text"ty :: type"} then @{text"ty list :: ordrel"}.
    7.17  Of course we should also define the meaning of @{text <<=} and
    7.18  @{text <<} on lists:
    7.19  *}
     8.1 --- a/doc-src/TutorialI/Types/Overloading1.thy	Sat Dec 01 18:51:46 2001 +0100
     8.2 +++ b/doc-src/TutorialI/Types/Overloading1.thy	Sat Dec 01 18:52:32 2001 +0100
     8.3 @@ -10,13 +10,12 @@
     8.4  introduce the class @{text ordrel}:
     8.5  *}
     8.6  
     8.7 -axclass ordrel < "term"
     8.8 +axclass ordrel < type
     8.9  
    8.10  text{*\noindent
    8.11  This introduces a new class @{text ordrel} and makes it a subclass of
    8.12 -the predefined class @{text term}, which
    8.13 -is the class of all HOL types.\footnote{The quotes around @{text term}
    8.14 -simply avoid the clash with the command \isacommand{term}.}
    8.15 +the predefined class @{text type}, which
    8.16 +is the class of all HOL types.
    8.17  This is a degenerate form of axiomatic type class without any axioms.
    8.18  Its sole purpose is to restrict the use of overloaded constants to meaningful
    8.19  instances:
     9.1 --- a/doc-src/TutorialI/Types/document/Overloading.tex	Sat Dec 01 18:51:46 2001 +0100
     9.2 +++ b/doc-src/TutorialI/Types/document/Overloading.tex	Sat Dec 01 18:52:32 2001 +0100
     9.3 @@ -2,16 +2,16 @@
     9.4  \begin{isabellebody}%
     9.5  \def\isabellecontext{Overloading}%
     9.6  \isamarkupfalse%
     9.7 -\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isachardoublequote}term{\isachardoublequote}{\isacharparenright}ordrel\isanewline
     9.8 +\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}ordrel\isanewline
     9.9  \isamarkupfalse%
    9.10  \isacommand{by}\ intro{\isacharunderscore}classes\isamarkupfalse%
    9.11  %
    9.12  \begin{isamarkuptext}%
    9.13  \noindent
    9.14  This \isacommand{instance} declaration can be read like the declaration of
    9.15 -a function on types.  The constructor \isa{list} maps types of class \isa{term} (all HOL types), to types of class \isa{ordrel};
    9.16 +a function on types.  The constructor \isa{list} maps types of class \isa{type} (all HOL types), to types of class \isa{ordrel};
    9.17  in other words,
    9.18 -if \isa{ty\ {\isacharcolon}{\isacharcolon}\ term} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}.
    9.19 +if \isa{ty\ {\isacharcolon}{\isacharcolon}\ type} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}.
    9.20  Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
    9.21  \isa{{\isacharless}{\isacharless}} on lists:%
    9.22  \end{isamarkuptext}%
    10.1 --- a/doc-src/TutorialI/Types/document/Overloading1.tex	Sat Dec 01 18:51:46 2001 +0100
    10.2 +++ b/doc-src/TutorialI/Types/document/Overloading1.tex	Sat Dec 01 18:52:32 2001 +0100
    10.3 @@ -14,14 +14,13 @@
    10.4  introduce the class \isa{ordrel}:%
    10.5  \end{isamarkuptext}%
    10.6  \isamarkuptrue%
    10.7 -\isacommand{axclass}\ ordrel\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isamarkupfalse%
    10.8 +\isacommand{axclass}\ ordrel\ {\isacharless}\ type\isamarkupfalse%
    10.9  %
   10.10  \begin{isamarkuptext}%
   10.11  \noindent
   10.12  This introduces a new class \isa{ordrel} and makes it a subclass of
   10.13 -the predefined class \isa{term}, which
   10.14 -is the class of all HOL types.\footnote{The quotes around \isa{term}
   10.15 -simply avoid the clash with the command \isacommand{term}.}
   10.16 +the predefined class \isa{type}, which
   10.17 +is the class of all HOL types.
   10.18  This is a degenerate form of axiomatic type class without any axioms.
   10.19  Its sole purpose is to restrict the use of overloaded constants to meaningful
   10.20  instances:%
    11.1 --- a/doc-src/TutorialI/tutorial.ind	Sat Dec 01 18:51:46 2001 +0100
    11.2 +++ b/doc-src/TutorialI/tutorial.ind	Sat Dec 01 18:52:32 2001 +0100
    11.3 @@ -90,7 +90,7 @@
    11.4    \item bisimulations, 106
    11.5    \item \isa {blast} (method), 79--80, 82
    11.6    \item \isa {bool} (type), 4, 5
    11.7 -  \item boolean expressions example, 19--22
    11.8 +  \item boolean expressions example, 20--22
    11.9    \item \isa {bspec} (theorem), \bold{98}
   11.10    \item \isacommand{by} (command), 63
   11.11  
   11.12 @@ -213,7 +213,7 @@
   11.13    \item flags, 5, 6, 33
   11.14      \subitem setting and resetting, 5
   11.15    \item \isa {force} (method), 81, 82
   11.16 -  \item formulae, 5
   11.17 +  \item formulae, 5--6
   11.18    \item forward proof, 82--88
   11.19    \item \isa {frule} (method), 73
   11.20    \item \isa {frule_tac} (method), 66
   11.21 @@ -254,7 +254,7 @@
   11.22    \item \isa {if} expressions, 5, 6
   11.23      \subitem simplification of, 33
   11.24      \subitem splitting of, 31, 49
   11.25 -  \item if-and-only-if, 5
   11.26 +  \item if-and-only-if, 6
   11.27    \item \isa {iff} (attribute), 80, 92, 120
   11.28    \item \isa {iffD1} (theorem), \bold{84}
   11.29    \item \isa {iffD2} (theorem), \bold{84}
   11.30 @@ -266,7 +266,7 @@
   11.31    \item \isa {impI} (theorem), \bold{62}
   11.32    \item implication, 62--63
   11.33    \item \isa {ind_cases} (method), 121
   11.34 -  \item \isa {induct_tac} (method), 12, 19, 52, 178
   11.35 +  \item \isa {induct_tac} (method), 12, 19, 51, 178
   11.36    \item induction, 174--181
   11.37      \subitem complete, 176
   11.38      \subitem deriving new schemas, 178
   11.39 @@ -326,7 +326,7 @@
   11.40    \item least number operator, \see{\protect\isa{LEAST}}{75}
   11.41    \item \isacommand {lemma} (command), 13
   11.42    \item \isacommand {lemmas} (command), 83, 92
   11.43 -  \item \isa {length} (symbol), 17
   11.44 +  \item \isa {length} (symbol), 18
   11.45    \item \isa {length_induct}, \bold{178}
   11.46    \item \isa {less_than} (constant), 104
   11.47    \item \isa {less_than_iff} (theorem), \bold{104}
   11.48 @@ -336,9 +336,10 @@
   11.49    \item lexicographic product, \bold{105}, 166
   11.50    \item {\texttt{lfp}}
   11.51      \subitem applications of, \see{CTL}{106}
   11.52 +  \item Library, 4
   11.53    \item linear arithmetic, 22--24, 139
   11.54    \item \isa {List} (theory), 17
   11.55 -  \item \isa {list} (type), 4, 9, 17
   11.56 +  \item \isa {list} (type), 5, 9, 17
   11.57    \item \isa {list.split} (theorem), 32
   11.58    \item \isa {lists_mono} (theorem), \bold{127}
   11.59    \item Lowe, Gavin, 184--185
   11.60 @@ -351,7 +352,7 @@
   11.61    \item measure functions, 47, 104
   11.62    \item \isa {measure_def} (theorem), \bold{105}
   11.63    \item meta-logic, \bold{70}
   11.64 -  \item methods, \bold{15}
   11.65 +  \item methods, \bold{16}
   11.66    \item \isa {min} (constant), 23, 24
   11.67    \item \isa {mod} (symbol), 23
   11.68    \item \isa {mod_div_equality} (theorem), \bold{141}
   11.69 @@ -377,8 +378,8 @@
   11.70    \item negation, 63--65
   11.71    \item \isa {Nil} (constant), 9
   11.72    \item \isa {no_asm} (modifier), 29
   11.73 -  \item \isa {no_asm_simp} (modifier), 29
   11.74 -  \item \isa {no_asm_use} (modifier), 29
   11.75 +  \item \isa {no_asm_simp} (modifier), 30
   11.76 +  \item \isa {no_asm_use} (modifier), 30
   11.77    \item non-standard reals, 145
   11.78    \item \isa {None} (constant), \bold{24}
   11.79    \item \isa {notE} (theorem), \bold{63}
   11.80 @@ -426,7 +427,7 @@
   11.81  
   11.82    \indexspace
   11.83  
   11.84 -  \item quantifiers, 5
   11.85 +  \item quantifiers, 6
   11.86      \subitem and inductive definitions, 125--127
   11.87      \subitem existential, 72
   11.88      \subitem for sets, 98
   11.89 @@ -483,7 +484,7 @@
   11.90  
   11.91    \item \isa {safe} (method), 81, 82
   11.92    \item safe rules, \bold{80}
   11.93 -  \item \isa {set} (type), 4, 95
   11.94 +  \item \isa {set} (type), 5, 95
   11.95    \item set comprehensions, 97--98
   11.96    \item \isa {set_ext} (theorem), \bold{96}
   11.97    \item sets, 95--99
   11.98 @@ -495,7 +496,7 @@
   11.99    \item \isa {simp} (attribute), 11, 28
  11.100    \item \isa {simp} (method), \bold{28}
  11.101    \item \isa {simp} del (attribute), 28
  11.102 -  \item \isa {simp_all} (method), 28, 37
  11.103 +  \item \isa {simp_all} (method), 29, 37
  11.104    \item simplification, 27--33, 163--166
  11.105      \subitem of \isa{let}-expressions, 31
  11.106      \subitem with definitions, 30
  11.107 @@ -569,7 +570,7 @@
  11.108    \item tuples, \see{pairs and tuples}{1}
  11.109    \item \isacommand {typ} (command), 16
  11.110    \item type constraints, \bold{6}
  11.111 -  \item type constructors, 4
  11.112 +  \item type constructors, 5
  11.113    \item type inference, \bold{5}
  11.114    \item type synonyms, 25
  11.115    \item type variables, 5
  11.116 @@ -597,14 +598,14 @@
  11.117      \subitem indexed, 98
  11.118    \item \isa {Union_iff} (theorem), \bold{98}
  11.119    \item \isa {unit} (type), 24
  11.120 -  \item unknowns, 6, \bold{58}
  11.121 +  \item unknowns, 7, \bold{58}
  11.122    \item unsafe rules, \bold{80}
  11.123    \item updating a function, \bold{99}
  11.124  
  11.125    \indexspace
  11.126  
  11.127 -  \item variables, 6--7
  11.128 -    \subitem schematic, 6
  11.129 +  \item variables, 7
  11.130 +    \subitem schematic, 7
  11.131      \subitem type, 5
  11.132    \item \isa {vimage_def} (theorem), \bold{101}
  11.133  
    12.1 --- a/src/HOL/AxClasses/Group.thy	Sat Dec 01 18:51:46 2001 +0100
    12.2 +++ b/src/HOL/AxClasses/Group.thy	Sat Dec 01 18:52:32 2001 +0100
    12.3 @@ -14,12 +14,12 @@
    12.4    one :: 'a
    12.5  
    12.6  
    12.7 -axclass monoid < "term"
    12.8 +axclass monoid < type
    12.9    assoc:      "(x [*] y) [*] z = x [*] (y [*] z)"
   12.10    left_unit:  "one [*] x = x"
   12.11    right_unit: "x [*] one = x"
   12.12  
   12.13 -axclass semigroup < "term"
   12.14 +axclass semigroup < type
   12.15    assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
   12.16  
   12.17  axclass group < semigroup
    13.1 --- a/src/HOL/AxClasses/Product.thy	Sat Dec 01 18:51:46 2001 +0100
    13.2 +++ b/src/HOL/AxClasses/Product.thy	Sat Dec 01 18:52:32 2001 +0100
    13.3 @@ -6,7 +6,7 @@
    13.4  
    13.5  theory Product = Main:
    13.6  
    13.7 -axclass product < "term"
    13.8 +axclass product < type
    13.9  
   13.10  consts
   13.11    product :: "'a::product => 'a => 'a"    (infixl "[*]" 70)
    14.1 --- a/src/HOL/AxClasses/Semigroups.thy	Sat Dec 01 18:51:46 2001 +0100
    14.2 +++ b/src/HOL/AxClasses/Semigroups.thy	Sat Dec 01 18:52:32 2001 +0100
    14.3 @@ -9,14 +9,14 @@
    14.4  consts
    14.5    times :: "'a => 'a => 'a"    (infixl "[*]" 70)
    14.6  
    14.7 -axclass semigroup < "term"
    14.8 +axclass semigroup < type
    14.9    assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
   14.10  
   14.11  
   14.12  consts
   14.13    plus :: "'a => 'a => 'a"    (infixl "[+]" 70)
   14.14  
   14.15 -axclass plus_semigroup < "term"
   14.16 +axclass plus_semigroup < type
   14.17    assoc: "(x [+] y) [+] z = x [+] (y [+] z)"
   14.18  
   14.19  end
    15.1 --- a/src/HOL/Divides.thy	Sat Dec 01 18:51:46 2001 +0100
    15.2 +++ b/src/HOL/Divides.thy	Sat Dec 01 18:52:32 2001 +0100
    15.3 @@ -11,7 +11,7 @@
    15.4  (*We use the same class for div and mod;
    15.5    moreover, dvd is defined whenever multiplication is*)
    15.6  axclass
    15.7 -  div < term
    15.8 +  div < type
    15.9  
   15.10  instance  nat :: div
   15.11  instance  nat :: plus_ac0 (add_commute,add_assoc,add_0)
    16.1 --- a/src/HOL/Finite.thy	Sat Dec 01 18:51:46 2001 +0100
    16.2 +++ b/src/HOL/Finite.thy	Sat Dec 01 18:52:32 2001 +0100
    16.3 @@ -18,7 +18,7 @@
    16.4  syntax finite :: 'a set => bool
    16.5  translations  "finite A"  ==  "A : Finites"
    16.6  
    16.7 -axclass	finite<term
    16.8 +axclass	finite < type
    16.9    finite "finite UNIV"
   16.10  
   16.11  (* This definition, although traditional, is ugly to work with
    17.1 --- a/src/HOL/Fun.ML	Sat Dec 01 18:51:46 2001 +0100
    17.2 +++ b/src/HOL/Fun.ML	Sat Dec 01 18:52:32 2001 +0100
    17.3 @@ -373,7 +373,7 @@
    17.4    fun mk_eq_cterm sg T l r = Thm.cterm_of sg (equals T $ l $ r)
    17.5  in 
    17.6    val fun_upd2_simproc = Simplifier.mk_simproc "fun_upd2"
    17.7 -   [Thm.read_cterm (sign_of (the_context ())) ("f(v:=w,x:=y)", HOLogic.termT)]
    17.8 +   [HOLogic.read_cterm (sign_of (the_context ())) "f(v := w, x := y)"]
    17.9     (fn sg => (K (fn t => case find_double t of (T,None)=> None | (T,Some rhs)=> 
   17.10         Some (prove_goalw_cterm [] (mk_eq_cterm sg T t rhs) fun_upd_prover))))
   17.11  end;
    18.1 --- a/src/HOL/Fun.thy	Sat Dec 01 18:51:46 2001 +0100
    18.2 +++ b/src/HOL/Fun.thy	Sat Dec 01 18:52:32 2001 +0100
    18.3 @@ -8,7 +8,7 @@
    18.4  
    18.5  Fun = Typedef +
    18.6  
    18.7 -instance set :: (term) order
    18.8 +instance set :: (type) order
    18.9                         (subset_refl,subset_trans,subset_antisym,psubset_eq)
   18.10  consts
   18.11    fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    19.1 --- a/src/HOL/HOL.thy	Sat Dec 01 18:51:46 2001 +0100
    19.2 +++ b/src/HOL/HOL.thy	Sat Dec 01 18:52:32 2001 +0100
    19.3 @@ -13,16 +13,16 @@
    19.4  
    19.5  subsubsection {* Core syntax *}
    19.6  
    19.7 -global
    19.8 +classes type < logic
    19.9 +defaultsort type
   19.10  
   19.11 -classes "term" < logic
   19.12 -defaultsort "term"
   19.13 +global
   19.14  
   19.15  typedecl bool
   19.16  
   19.17  arities
   19.18 -  bool :: "term"
   19.19 -  fun :: ("term", "term") "term"
   19.20 +  bool :: type
   19.21 +  fun :: (type, type) type
   19.22  
   19.23  judgment
   19.24    Trueprop      :: "bool => prop"                   ("(_)" 5)
   19.25 @@ -145,12 +145,12 @@
   19.26  
   19.27  subsubsection {* Generic algebraic operations *}
   19.28  
   19.29 -axclass zero < "term"
   19.30 -axclass one < "term"
   19.31 -axclass plus < "term"
   19.32 -axclass minus < "term"
   19.33 -axclass times < "term"
   19.34 -axclass inverse < "term"
   19.35 +axclass zero < type
   19.36 +axclass one < type
   19.37 +axclass plus < type
   19.38 +axclass minus < type
   19.39 +axclass times < type
   19.40 +axclass inverse < type
   19.41  
   19.42  global
   19.43  
   19.44 @@ -528,7 +528,7 @@
   19.45  subsection {* Order signatures and orders *}
   19.46  
   19.47  axclass
   19.48 -  ord < "term"
   19.49 +  ord < type
   19.50  
   19.51  syntax
   19.52    "op <"        :: "['a::ord, 'a] => bool"             ("op <")
    20.1 --- a/src/HOL/IMP/Com.thy	Sat Dec 01 18:51:46 2001 +0100
    20.2 +++ b/src/HOL/IMP/Com.thy	Sat Dec 01 18:52:32 2001 +0100
    20.3 @@ -16,7 +16,7 @@
    20.4        aexp  = state => val
    20.5        bexp  = state => bool
    20.6  
    20.7 -arities loc :: term
    20.8 +arities loc :: type
    20.9  
   20.10  datatype
   20.11    com = SKIP
    21.1 --- a/src/HOL/IMP/Expr.thy	Sat Dec 01 18:51:46 2001 +0100
    21.2 +++ b/src/HOL/IMP/Expr.thy	Sat Dec 01 18:52:32 2001 +0100
    21.3 @@ -15,7 +15,7 @@
    21.4        n2n = "nat => nat"
    21.5        n2n2n = "nat => nat => nat"
    21.6  
    21.7 -arities loc :: term
    21.8 +arities loc :: type
    21.9  
   21.10  datatype
   21.11    aexp = N nat
    22.1 --- a/src/HOL/IMPP/Com.thy	Sat Dec 01 18:51:46 2001 +0100
    22.2 +++ b/src/HOL/IMPP/Com.thy	Sat Dec 01 18:52:32 2001 +0100
    22.3 @@ -12,7 +12,7 @@
    22.4                          current Isabelle, types cannot be refined later *)
    22.5  types	 glb
    22.6           loc
    22.7 -arities	 (*val,*)glb,loc :: term
    22.8 +arities	 (*val,*)glb,loc :: type
    22.9  consts   Arg, Res :: loc
   22.10  
   22.11  datatype vname  = Glb glb | Loc loc
   22.12 @@ -21,14 +21,14 @@
   22.13  datatype state  = st globs locals
   22.14  (* for the meta theory, the following would be sufficient:
   22.15  types    state
   22.16 -arities  state::term
   22.17 +arities  state::type
   22.18  consts   st:: [globs , locals] => state
   22.19  *)
   22.20  types	 aexp   = state => val
   22.21  	 bexp   = state => bool
   22.22  
   22.23  types	pname
   22.24 -arities	pname  :: term
   22.25 +arities	pname  :: type
   22.26  
   22.27  datatype com
   22.28        = SKIP
    23.1 --- a/src/HOL/Induct/Com.thy	Sat Dec 01 18:51:46 2001 +0100
    23.2 +++ b/src/HOL/Induct/Com.thy	Sat Dec 01 18:52:32 2001 +0100
    23.3 @@ -12,7 +12,7 @@
    23.4        state = "loc => nat"
    23.5        n2n2n = "nat => nat => nat"
    23.6  
    23.7 -arities loc :: term
    23.8 +arities loc :: type
    23.9  
   23.10  datatype
   23.11    exp = N nat
    24.1 --- a/src/HOL/Integ/Bin.ML	Sat Dec 01 18:51:46 2001 +0100
    24.2 +++ b/src/HOL/Integ/Bin.ML	Sat Dec 01 18:52:32 2001 +0100
    24.3 @@ -349,7 +349,7 @@
    24.4    fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg []
    24.5  
    24.6    fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc
    24.7 -  fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.termT)
    24.8 +  fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context())) s
    24.9    val prep_pats = map prep_pat
   24.10  
   24.11    fun is_numeral (Const("Numeral.number_of", _) $ w) = true
    25.1 --- a/src/HOL/Integ/nat_simprocs.ML	Sat Dec 01 18:51:46 2001 +0100
    25.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Sat Dec 01 18:52:32 2001 +0100
    25.3 @@ -169,8 +169,7 @@
    25.4                  bin_arith_simps @ bin_rel_simps;
    25.5  
    25.6  fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
    25.7 -fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ()))
    25.8 -                                (s, HOLogic.termT);
    25.9 +fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context ())) s;
   25.10  val prep_pats = map prep_pat;
   25.11  
   25.12  
    26.1 --- a/src/HOL/Lattice/Lattice.thy	Sat Dec 01 18:51:46 2001 +0100
    26.2 +++ b/src/HOL/Lattice/Lattice.thy	Sat Dec 01 18:52:32 2001 +0100
    26.3 @@ -519,7 +519,7 @@
    26.4    qed
    26.5  qed
    26.6  
    26.7 -instance fun :: ("term", lattice) lattice
    26.8 +instance fun :: (type, lattice) lattice
    26.9  proof
   26.10    fix f g :: "'a \<Rightarrow> 'b::lattice"
   26.11    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!? *)
    27.1 --- a/src/HOL/Lattice/Orders.thy	Sat Dec 01 18:51:46 2001 +0100
    27.2 +++ b/src/HOL/Lattice/Orders.thy	Sat Dec 01 18:52:32 2001 +0100
    27.3 @@ -18,7 +18,7 @@
    27.4    required to be related (in either direction).
    27.5  *}
    27.6  
    27.7 -axclass leq < "term"
    27.8 +axclass leq < type
    27.9  consts
   27.10    leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "[=" 50)
   27.11  syntax (xsymbols)
   27.12 @@ -249,7 +249,7 @@
   27.13    orders need \emph{not} be linear in general.
   27.14  *}
   27.15  
   27.16 -instance fun :: ("term", leq) leq ..
   27.17 +instance fun :: (type, leq) leq ..
   27.18  
   27.19  defs (overloaded)
   27.20    leq_fun_def: "f \<sqsubseteq> g \<equiv> \<forall>x. f x \<sqsubseteq> g x"
   27.21 @@ -260,7 +260,7 @@
   27.22  lemma leq_funD [dest?]: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
   27.23    by (unfold leq_fun_def) blast
   27.24  
   27.25 -instance fun :: ("term", quasi_order) quasi_order
   27.26 +instance fun :: (type, quasi_order) quasi_order
   27.27  proof
   27.28    fix f g h :: "'a \<Rightarrow> 'b::quasi_order"
   27.29    show "f \<sqsubseteq> f"
   27.30 @@ -276,7 +276,7 @@
   27.31    qed
   27.32  qed
   27.33  
   27.34 -instance fun :: ("term", partial_order) partial_order
   27.35 +instance fun :: (type, partial_order) partial_order
   27.36  proof
   27.37    fix f g :: "'a \<Rightarrow> 'b::partial_order"
   27.38    assume fg: "f \<sqsubseteq> g" and gf: "g \<sqsubseteq> f"
    28.1 --- a/src/HOL/Library/List_Prefix.thy	Sat Dec 01 18:51:46 2001 +0100
    28.2 +++ b/src/HOL/Library/List_Prefix.thy	Sat Dec 01 18:52:32 2001 +0100
    28.3 @@ -13,13 +13,13 @@
    28.4  
    28.5  subsection {* Prefix order on lists *}
    28.6  
    28.7 -instance list :: ("term") ord ..
    28.8 +instance list :: (type) ord ..
    28.9  
   28.10  defs (overloaded)
   28.11    prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs"
   28.12    strict_prefix_def: "xs < ys == xs \<le> ys \<and> xs \<noteq> (ys::'a list)"
   28.13  
   28.14 -instance list :: ("term") order
   28.15 +instance list :: (type) order
   28.16    by intro_classes (auto simp add: prefix_def strict_prefix_def)
   28.17  
   28.18  lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"
    29.1 --- a/src/HOL/Library/Multiset.thy	Sat Dec 01 18:51:46 2001 +0100
    29.2 +++ b/src/HOL/Library/Multiset.thy	Sat Dec 01 18:52:32 2001 +0100
    29.3 @@ -47,9 +47,9 @@
    29.4    set_of :: "'a multiset => 'a set"
    29.5    "set_of M == {x. x :# M}"
    29.6  
    29.7 -instance multiset :: ("term") plus ..
    29.8 -instance multiset :: ("term") minus ..
    29.9 -instance multiset :: ("term") zero ..
   29.10 +instance multiset :: (type) plus ..
   29.11 +instance multiset :: (type) minus ..
   29.12 +instance multiset :: (type) zero ..
   29.13  
   29.14  defs (overloaded)
   29.15    union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
   29.16 @@ -114,7 +114,7 @@
   29.17  
   29.18  theorems union_ac = union_assoc union_commute union_lcomm
   29.19  
   29.20 -instance multiset :: ("term") plus_ac0
   29.21 +instance multiset :: (type) plus_ac0
   29.22    apply intro_classes
   29.23      apply (rule union_commute)
   29.24     apply (rule union_assoc)
   29.25 @@ -660,7 +660,7 @@
   29.26  
   29.27  subsubsection {* Partial-order properties *}
   29.28  
   29.29 -instance multiset :: ("term") ord ..
   29.30 +instance multiset :: (type) ord ..
   29.31  
   29.32  defs (overloaded)
   29.33    less_multiset_def: "M' < M == (M', M) \<in> mult {(x', x). x' < x}"
    30.1 --- a/src/HOL/Library/Quotient.thy	Sat Dec 01 18:51:46 2001 +0100
    30.2 +++ b/src/HOL/Library/Quotient.thy	Sat Dec 01 18:52:32 2001 +0100
    30.3 @@ -23,7 +23,7 @@
    30.4   "\<sim> :: 'a => 'a => bool"}.
    30.5  *}
    30.6  
    30.7 -axclass eqv \<subseteq> "term"
    30.8 +axclass eqv \<subseteq> type
    30.9  consts
   30.10    eqv :: "('a::eqv) => 'a => bool"    (infixl "\<sim>" 50)
   30.11  
    31.1 --- a/src/HOL/MicroJava/J/Type.thy	Sat Dec 01 18:51:46 2001 +0100
    31.2 +++ b/src/HOL/MicroJava/J/Type.thy	Sat Dec 01 18:52:32 2001 +0100
    31.3 @@ -11,9 +11,6 @@
    31.4  typedecl cname  (* class name *)
    31.5  typedecl vnam   (* variable or field name *)
    31.6  typedecl mname  (* method name *)
    31.7 -arities  cname :: "term"
    31.8 -         vnam  :: "term"
    31.9 -         mname :: "term"
   31.10  
   31.11  datatype vname    (* names for This pointer and local/field variables *)
   31.12    = This
    32.1 --- a/src/HOL/MicroJava/J/Value.thy	Sat Dec 01 18:51:46 2001 +0100
    32.2 +++ b/src/HOL/MicroJava/J/Value.thy	Sat Dec 01 18:52:32 2001 +0100
    32.3 @@ -9,7 +9,6 @@
    32.4  theory Value = Type:
    32.5  
    32.6  typedecl loc (* locations, i.e. abstract references on objects *)
    32.7 -arities loc :: "term"
    32.8  
    32.9  datatype val
   32.10    = Unit        (* dummy result value of void methods *)
    33.1 --- a/src/HOL/MiniML/Type.thy	Sat Dec 01 18:51:46 2001 +0100
    33.2 +++ b/src/HOL/MiniML/Type.thy	Sat Dec 01 18:52:32 2001 +0100
    33.3 @@ -9,7 +9,7 @@
    33.4  Type = Maybe + 
    33.5  
    33.6  (* new class for structures containing type variables *)
    33.7 -axclass  type_struct < term 
    33.8 +axclass  type_struct < type
    33.9  
   33.10  
   33.11  (* type expressions *)
   33.12 @@ -33,7 +33,7 @@
   33.13  instance  typ::type_struct
   33.14  instance  type_scheme::type_struct  
   33.15  instance  list::(type_struct)type_struct
   33.16 -instance  fun::(term,type_struct)type_struct
   33.17 +instance  fun::(type,type_struct)type_struct
   33.18  
   33.19  
   33.20  (* free_tv s: the type variables occuring freely in the type structure s *)
    34.1 --- a/src/HOL/Nat.thy	Sat Dec 01 18:51:46 2001 +0100
    34.2 +++ b/src/HOL/Nat.thy	Sat Dec 01 18:52:32 2001 +0100
    34.3 @@ -19,7 +19,7 @@
    34.4  instance nat :: linorder (nat_le_linear)
    34.5  instance nat :: wellorder (wf_less)
    34.6  
    34.7 -axclass power < term
    34.8 +axclass power < type
    34.9  
   34.10  consts
   34.11    power :: ['a::power, nat] => 'a            (infixr "^" 80)
    35.1 --- a/src/HOL/NatDef.thy	Sat Dec 01 18:51:46 2001 +0100
    35.2 +++ b/src/HOL/NatDef.thy	Sat Dec 01 18:52:32 2001 +0100
    35.3 @@ -12,13 +12,8 @@
    35.4  
    35.5  (** type ind **)
    35.6  
    35.7 -global
    35.8 -
    35.9 -types
   35.10 -  ind
   35.11 -
   35.12 -arities
   35.13 -  ind :: term
   35.14 +types ind
   35.15 +arities ind :: type
   35.16  
   35.17  consts
   35.18    Zero_Rep      :: ind
   35.19 @@ -43,6 +38,8 @@
   35.20    Zero_RepI "Zero_Rep : Nat'"
   35.21    Suc_RepI  "i : Nat' ==> Suc_Rep i : Nat'"
   35.22  
   35.23 +global
   35.24 +
   35.25  typedef (Nat)
   35.26    nat = "Nat'"   (Nat'.Zero_RepI)
   35.27  
    36.1 --- a/src/HOL/Numeral.thy	Sat Dec 01 18:51:46 2001 +0100
    36.2 +++ b/src/HOL/Numeral.thy	Sat Dec 01 18:52:32 2001 +0100
    36.3 @@ -14,7 +14,7 @@
    36.4        | Bit bin bool    (infixl "BIT" 90)
    36.5  
    36.6  axclass
    36.7 -  number < "term"      (*for numeric types: nat, int, real, ...*)
    36.8 +  number < type  -- {* for numeric types: nat, int, real, \dots *}
    36.9  
   36.10  consts
   36.11    number_of :: "bin => 'a::number"
    37.1 --- a/src/HOL/Product_Type.thy	Sat Dec 01 18:51:46 2001 +0100
    37.2 +++ b/src/HOL/Product_Type.thy	Sat Dec 01 18:52:32 2001 +0100
    37.3 @@ -342,8 +342,8 @@
    37.4          (cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
    37.5          (K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
    37.6    val sign = sign_of (the_context ());
    37.7 -  fun simproc name patstr = Simplifier.mk_simproc name
    37.8 -                [Thm.read_cterm sign (patstr, HOLogic.termT)];
    37.9 +  fun simproc name patstr =
   37.10 +    Simplifier.mk_simproc name [HOLogic.read_cterm sign patstr];
   37.11  
   37.12    val beta_patstr = "split f z";
   37.13    val  eta_patstr = "split f";
    38.1 --- a/src/HOL/Prolog/Func.thy	Sat Dec 01 18:51:46 2001 +0100
    38.2 +++ b/src/HOL/Prolog/Func.thy	Sat Dec 01 18:52:32 2001 +0100
    38.3 @@ -4,7 +4,7 @@
    38.4  
    38.5  types tm
    38.6  
    38.7 -arities tm :: term
    38.8 +arities tm :: type
    38.9  
   38.10  consts	abs	:: (tm => tm) => tm
   38.11  	app	:: tm => tm => tm
    39.1 --- a/src/HOL/Prolog/Test.thy	Sat Dec 01 18:51:46 2001 +0100
    39.2 +++ b/src/HOL/Prolog/Test.thy	Sat Dec 01 18:52:32 2001 +0100
    39.3 @@ -3,10 +3,10 @@
    39.4  Test = HOHH +
    39.5  
    39.6  types nat
    39.7 -arities nat :: term
    39.8 +arities nat :: type
    39.9  
   39.10  types 'a list
   39.11 -arities list :: (term) term
   39.12 +arities list :: (type) type
   39.13  
   39.14  consts Nil   :: 'a list		 	 		 ("[]")
   39.15         Cons  :: 'a => 'a list => 'a list		 (infixr "#"  65)
   39.16 @@ -20,7 +20,7 @@
   39.17    "[x]"         == "x#[]"
   39.18  
   39.19  types   person
   39.20 -arities person  :: term
   39.21 +arities person  :: type
   39.22  
   39.23  consts  
   39.24  	append  :: ['a list, 'a list, 'a list]		  => bool
    40.1 --- a/src/HOL/Prolog/Type.thy	Sat Dec 01 18:51:46 2001 +0100
    40.2 +++ b/src/HOL/Prolog/Type.thy	Sat Dec 01 18:52:32 2001 +0100
    40.3 @@ -4,7 +4,7 @@
    40.4  
    40.5  types ty
    40.6  
    40.7 -arities ty :: term
    40.8 +arities ty :: type
    40.9  
   40.10  consts  bool	:: ty
   40.11  	nat	:: ty
    41.1 --- a/src/HOL/Real/RealBin.ML	Sat Dec 01 18:51:46 2001 +0100
    41.2 +++ b/src/HOL/Real/RealBin.ML	Sat Dec 01 18:52:32 2001 +0100
    41.3 @@ -403,7 +403,7 @@
    41.4   	  real_mult_0, real_mult_0_right, real_mult_1, real_mult_1_right];
    41.5  
    41.6  fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
    41.7 -fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.termT);
    41.8 +fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context ())) s;
    41.9  val prep_pats = map prep_pat;
   41.10  
   41.11  structure CancelNumeralsCommon =
    42.1 --- a/src/HOL/Relation_Power.thy	Sat Dec 01 18:51:46 2001 +0100
    42.2 +++ b/src/HOL/Relation_Power.thy	Sat Dec 01 18:52:32 2001 +0100
    42.3 @@ -15,7 +15,7 @@
    42.4  Relation_Power = Nat +
    42.5  
    42.6  instance
    42.7 -  set :: (term) {power}   (* only ('a * 'a) set should be in power! *)
    42.8 +  set :: (type) power   (* only ('a * 'a) set should be in power! *)
    42.9  
   42.10  primrec (relpow)
   42.11    "R^0 = Id"
   42.12 @@ -23,7 +23,7 @@
   42.13  
   42.14  
   42.15  instance
   42.16 -  fun :: (term,term)power   (* only 'a => 'a should be in power! *)
   42.17 +  fun :: (type, type) power   (* only 'a => 'a should be in power! *)
   42.18  
   42.19  primrec (funpow)
   42.20    "f^0 = id"
    43.1 --- a/src/HOL/Set.thy	Sat Dec 01 18:51:46 2001 +0100
    43.2 +++ b/src/HOL/Set.thy	Sat Dec 01 18:52:32 2001 +0100
    43.3 @@ -17,7 +17,7 @@
    43.4  global
    43.5  
    43.6  typedecl 'a set
    43.7 -arities set :: ("term") "term"
    43.8 +arities set :: (type) type
    43.9  
   43.10  consts
   43.11    "{}"          :: "'a set"                             ("{}")
   43.12 @@ -42,8 +42,8 @@
   43.13  
   43.14  local
   43.15  
   43.16 -instance set :: ("term") ord ..
   43.17 -instance set :: ("term") minus ..
   43.18 +instance set :: (type) ord ..
   43.19 +instance set :: (type) minus ..
   43.20  
   43.21  
   43.22  subsection {* Additional concrete syntax *}
    44.1 --- a/src/HOL/TLA/Init.thy	Sat Dec 01 18:51:46 2001 +0100
    44.2 +++ b/src/HOL/TLA/Init.thy	Sat Dec 01 18:52:32 2001 +0100
    44.3 @@ -17,7 +17,7 @@
    44.4    temporal = behavior form
    44.5  
    44.6  arities
    44.7 -  behavior    :: term
    44.8 +  behavior    :: type
    44.9  
   44.10  instance
   44.11    behavior    :: world
    45.1 --- a/src/HOL/TLA/Intensional.thy	Sat Dec 01 18:51:46 2001 +0100
    45.2 +++ b/src/HOL/TLA/Intensional.thy	Sat Dec 01 18:52:32 2001 +0100
    45.3 @@ -13,12 +13,12 @@
    45.4  Intensional  =  Main +
    45.5  
    45.6  axclass
    45.7 -  world < term
    45.8 +  world < type
    45.9  
   45.10  (** abstract syntax **)
   45.11  
   45.12  types
   45.13 -  ('w,'a) expr = 'w => 'a               (* intention: 'w::world, 'a::term *)
   45.14 +  ('w,'a) expr = 'w => 'a               (* intention: 'w::world, 'a::type *)
   45.15    'w form = ('w, bool) expr
   45.16  
   45.17  consts
    46.1 --- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Sat Dec 01 18:51:46 2001 +0100
    46.2 +++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Sat Dec 01 18:52:32 2001 +0100
    46.3 @@ -21,7 +21,7 @@
    46.4    ('a,'r) channel = (PrIds => ('a,'r) chan) stfun
    46.5  
    46.6  arities
    46.7 -  chan :: (term,term) term
    46.8 +  chan :: (type,type) type
    46.9  
   46.10  consts
   46.11    (* data-level functions *)
    47.1 --- a/src/HOL/TLA/Stfun.thy	Sat Dec 01 18:51:46 2001 +0100
    47.2 +++ b/src/HOL/TLA/Stfun.thy	Sat Dec 01 18:52:32 2001 +0100
    47.3 @@ -17,7 +17,7 @@
    47.4      stpred   = "bool stfun"
    47.5  
    47.6  arities
    47.7 -  state :: term
    47.8 +  state :: type
    47.9  
   47.10  instance
   47.11    state :: world
    48.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Sat Dec 01 18:51:46 2001 +0100
    48.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sat Dec 01 18:52:32 2001 +0100
    48.3 @@ -120,7 +120,7 @@
    48.4            (1 upto (length descr'))));
    48.5  
    48.6      val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
    48.7 -      replicate (length descr') HOLogic.termS);
    48.8 +      replicate (length descr') HOLogic.typeS);
    48.9  
   48.10      val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
   48.11        map (fn (_, cargs) =>
   48.12 @@ -302,7 +302,7 @@
   48.13      val recTs = get_rec_types descr' sorts;
   48.14      val used = foldr add_typ_tfree_names (recTs, []);
   48.15      val newTs = take (length (hd descr), recTs);
   48.16 -    val T' = TFree (variant used "'t", HOLogic.termS);
   48.17 +    val T' = TFree (variant used "'t", HOLogic.typeS);
   48.18  
   48.19      fun mk_dummyT (DtRec _) = T'
   48.20        | mk_dummyT (DtType ("fun", [T, _])) = typ_of_dtyp descr' sorts T --> T'
    49.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Dec 01 18:51:46 2001 +0100
    49.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Dec 01 18:52:32 2001 +0100
    49.3 @@ -365,7 +365,7 @@
    49.4     | _ => None)
    49.5    | distinct_proc sg _ _ = None;
    49.6  
    49.7 -val distinct_pats = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s = t", HOLogic.termT)];
    49.8 +val distinct_pats = [HOLogic.read_cterm (Theory.sign_of HOL.thy) "s = t"];
    49.9  val distinct_simproc = mk_simproc distinctN distinct_pats distinct_proc;
   49.10  
   49.11  val dist_ss = HOL_ss addsimprocs [distinct_simproc];
   49.12 @@ -460,7 +460,7 @@
   49.13            (constrs ~~ constr_syntax')) ((hd descr) ~~ newTs ~~ constr_syntax);
   49.14  
   49.15      val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
   49.16 -      replicate (length descr') HOLogic.termS);
   49.17 +      replicate (length descr') HOLogic.typeS);
   49.18  
   49.19      val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
   49.20        map (fn (_, cargs) =>
   49.21 @@ -484,7 +484,7 @@
   49.22      val size_names = DatatypeProp.indexify_names
   49.23        (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs)));
   49.24  
   49.25 -    val freeT = TFree (variant used "'t", HOLogic.termS);
   49.26 +    val freeT = TFree (variant used "'t", HOLogic.typeS);
   49.27      val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
   49.28        map (fn (_, cargs) =>
   49.29          let val Ts = map (typ_of_dtyp descr' sorts) cargs
    50.1 --- a/src/HOL/Tools/datatype_prop.ML	Sat Dec 01 18:51:46 2001 +0100
    50.2 +++ b/src/HOL/Tools/datatype_prop.ML	Sat Dec 01 18:52:32 2001 +0100
    50.3 @@ -177,7 +177,7 @@
    50.4      val used = foldr add_typ_tfree_names (recTs, []);
    50.5  
    50.6      val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
    50.7 -      replicate (length descr') HOLogic.termS);
    50.8 +      replicate (length descr') HOLogic.typeS);
    50.9  
   50.10      val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
   50.11        map (fn (_, cargs) =>
   50.12 @@ -241,7 +241,7 @@
   50.13      val recTs = get_rec_types descr' sorts;
   50.14      val used = foldr add_typ_tfree_names (recTs, []);
   50.15      val newTs = take (length (hd descr), recTs);
   50.16 -    val T' = TFree (variant used "'t", HOLogic.termS);
   50.17 +    val T' = TFree (variant used "'t", HOLogic.typeS);
   50.18  
   50.19      val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
   50.20        map (fn (_, cargs) =>
   50.21 @@ -326,7 +326,7 @@
   50.22      val recTs = get_rec_types descr' sorts;
   50.23      val used' = foldr add_typ_tfree_names (recTs, []);
   50.24      val newTs = take (length (hd descr), recTs);
   50.25 -    val T' = TFree (variant used' "'t", HOLogic.termS);
   50.26 +    val T' = TFree (variant used' "'t", HOLogic.typeS);
   50.27      val P = Free ("P", T' --> HOLogic.boolT);
   50.28  
   50.29      fun make_split (((_, (_, _, constrs)), T), comb_t) =
    51.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Dec 01 18:51:46 2001 +0100
    51.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Dec 01 18:52:32 2001 +0100
    51.3 @@ -838,7 +838,7 @@
    51.4  fun add_inductive verbose coind c_strings intro_srcs raw_monos thy =
    51.5    let
    51.6      val sign = Theory.sign_of thy;
    51.7 -    val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
    51.8 +    val cs = map (term_of o HOLogic.read_cterm sign) c_strings;
    51.9  
   51.10      val intr_names = map (fst o fst) intro_srcs;
   51.11      fun read_rule s = Thm.read_cterm sign (s, propT)
    52.1 --- a/src/HOL/Tools/record_package.ML	Sat Dec 01 18:51:46 2001 +0100
    52.2 +++ b/src/HOL/Tools/record_package.ML	Sat Dec 01 18:52:32 2001 +0100
    52.3 @@ -493,7 +493,7 @@
    52.4  
    52.5  local
    52.6  
    52.7 -val sel_upd_pat = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s (u k r)", HOLogic.termT)];
    52.8 +val sel_upd_pat = [HOLogic.read_cterm (Theory.sign_of HOL.thy) "s (u k r)"];
    52.9  
   52.10  fun proc sg _ t =
   52.11    (case t of (sel as Const (s, _)) $ ((upd as Const (u, _)) $ k $ r) =>
   52.12 @@ -560,7 +560,7 @@
   52.13  fun field_typedefs zeta moreT names theory =
   52.14    let
   52.15      val alpha = "'a";
   52.16 -    val aT = TFree (alpha, HOLogic.termS);
   52.17 +    val aT = TFree (alpha, HOLogic.typeS);
   52.18      val UNIV = HOLogic.mk_UNIV (HOLogic.mk_prodT (aT, moreT));
   52.19  
   52.20      fun type_def (thy, name) =
   52.21 @@ -581,7 +581,7 @@
   52.22      val base = Sign.base_name;
   52.23      val full_path = Sign.full_name_path sign;
   52.24  
   52.25 -    val xT = TFree (variant alphas "'x", HOLogic.termS);
   52.26 +    val xT = TFree (variant alphas "'x", HOLogic.typeS);
   52.27  
   52.28  
   52.29      (* prepare declarations and definitions *)
   52.30 @@ -683,7 +683,7 @@
   52.31      val all_named_vars = parent_named_vars @ named_vars;
   52.32  
   52.33      val zeta = variant alphas "'z";
   52.34 -    val moreT = TFree (zeta, HOLogic.termS);
   52.35 +    val moreT = TFree (zeta, HOLogic.typeS);
   52.36      val more = Free (moreN, moreT);
   52.37      val full_moreN = full moreN;
   52.38      fun more_part t = mk_more t full_moreN;
    53.1 --- a/src/HOL/Tools/typedef_package.ML	Sat Dec 01 18:51:46 2001 +0100
    53.2 +++ b/src/HOL/Tools/typedef_package.ML	Sat Dec 01 18:52:32 2001 +0100
    53.3 @@ -58,7 +58,7 @@
    53.4      val full = Sign.full_name (Theory.sign_of thy);
    53.5  
    53.6      fun arity_of (raw_name, args, mx) =
    53.7 -      (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.termS, HOLogic.termS);
    53.8 +      (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.typeS, HOLogic.typeS);
    53.9    in
   53.10      if can (Theory.assert_super HOL.thy) thy then
   53.11        thy
   53.12 @@ -97,7 +97,7 @@
   53.13  (* prepare_typedef *)
   53.14  
   53.15  fun read_term sg used s =
   53.16 -  #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.termT));
   53.17 +  #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.typeT));
   53.18  
   53.19  fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg;
   53.20  
   53.21 @@ -125,7 +125,7 @@
   53.22      val goal_pat = mk_nonempty (Var (vname, setT));
   53.23  
   53.24      (*lhs*)
   53.25 -    val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs;
   53.26 +    val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.typeS)) vs;
   53.27      val tname = Syntax.type_name t mx;
   53.28      val full_tname = full tname;
   53.29      val newT = Type (full_tname, map TFree lhs_tfrees);
   53.30 @@ -162,7 +162,9 @@
   53.31            fun make th = Drule.standard (th OF [type_definition]);
   53.32            val (theory'', [Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
   53.33                Rep_cases, Abs_cases, Rep_induct, Abs_induct]) =
   53.34 -            theory' |> PureThy.add_thms
   53.35 +            theory'
   53.36 +            |> Theory.add_path name
   53.37 +            |> PureThy.add_thms
   53.38                ([((Rep_name, make Rep), []),
   53.39                  ((Rep_name ^ "_inverse", make Rep_inverse), []),
   53.40                  ((Abs_name ^ "_inverse", make Abs_inverse), []),
   53.41 @@ -175,7 +177,8 @@
   53.42                  ((Rep_name ^ "_induct", make Rep_induct),
   53.43                    [RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]),
   53.44                  ((Abs_name ^ "_induct", make Abs_induct),
   53.45 -                  [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])]);
   53.46 +                  [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])])
   53.47 +            |>> Theory.parent_path;
   53.48            val result = {type_definition = type_definition, set_def = set_def,
   53.49              Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
   53.50              Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
    54.1 --- a/src/HOL/UNITY/Comp.thy	Sat Dec 01 18:51:46 2001 +0100
    54.2 +++ b/src/HOL/UNITY/Comp.thy	Sat Dec 01 18:52:32 2001 +0100
    54.3 @@ -16,7 +16,7 @@
    54.4  Comp = Union +
    54.5  
    54.6  instance
    54.7 -  program :: (term)ord
    54.8 +  program :: (type) ord
    54.9  
   54.10  defs
   54.11    component_def   "F <= H == EX G. F Join G = H"
    55.1 --- a/src/HOL/UNITY/Comp/Counterc.thy	Sat Dec 01 18:51:46 2001 +0100
    55.2 +++ b/src/HOL/UNITY/Comp/Counterc.thy	Sat Dec 01 18:52:32 2001 +0100
    55.3 @@ -13,7 +13,7 @@
    55.4  
    55.5  Counterc =  Comp +
    55.6  types state
    55.7 -arities state :: term
    55.8 +arities state :: type
    55.9  
   55.10  consts
   55.11    C :: "state=>int"
    56.1 --- a/src/HOL/UNITY/Comp/PriorityAux.thy	Sat Dec 01 18:51:46 2001 +0100
    56.2 +++ b/src/HOL/UNITY/Comp/PriorityAux.thy	Sat Dec 01 18:52:32 2001 +0100
    56.3 @@ -6,10 +6,10 @@
    56.4  Auxiliary definitions needed in Priority.thy
    56.5  *)
    56.6  
    56.7 -PriorityAux  =  Main +
    56.8 +PriorityAux = Main +
    56.9  
   56.10  types vertex
   56.11 -arities vertex::term
   56.12 +arities vertex :: type
   56.13    
   56.14  constdefs
   56.15    (* symmetric closure: removes the orientation of a relation *)
    57.1 --- a/src/HOL/UNITY/Extend.ML	Sat Dec 01 18:51:46 2001 +0100
    57.2 +++ b/src/HOL/UNITY/Extend.ML	Sat Dec 01 18:52:32 2001 +0100
    57.3 @@ -125,7 +125,7 @@
    57.4  
    57.5  (** A sequence of proof steps borrowed from Provers/split_paired_all.ML **)
    57.6  
    57.7 -val cT = TFree ("'c", ["term"]);
    57.8 +val cT = TFree ("'c", HOLogic.typeS);
    57.9  
   57.10  (* "PROP P x == PROP P (h (f x, g x))" *)
   57.11  val lemma1 = Thm.combination
    58.1 --- a/src/HOL/UNITY/GenPrefix.thy	Sat Dec 01 18:51:46 2001 +0100
    58.2 +++ b/src/HOL/UNITY/GenPrefix.thy	Sat Dec 01 18:52:32 2001 +0100
    58.3 @@ -27,7 +27,7 @@
    58.4  
    58.5      append  "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)"
    58.6  
    58.7 -instance list :: (term)ord
    58.8 +instance list :: (type)ord
    58.9  
   58.10  defs
   58.11    prefix_def        "xs <= zs  ==  (xs,zs) : genPrefix Id"
    59.1 --- a/src/HOL/UNITY/Guar.thy	Sat Dec 01 18:51:46 2001 +0100
    59.2 +++ b/src/HOL/UNITY/Guar.thy	Sat Dec 01 18:52:32 2001 +0100
    59.3 @@ -20,7 +20,7 @@
    59.4  
    59.5  Guar = Comp +
    59.6  
    59.7 -instance program :: (term) order
    59.8 +instance program :: (type) order
    59.9                      (component_refl, component_trans, component_antisym,
   59.10                       program_less_le)
   59.11  
    60.1 --- a/src/HOL/UNITY/ListOrder.thy	Sat Dec 01 18:51:46 2001 +0100
    60.2 +++ b/src/HOL/UNITY/ListOrder.thy	Sat Dec 01 18:52:32 2001 +0100
    60.3 @@ -8,7 +8,7 @@
    60.4  
    60.5  ListOrder = GenPrefix +
    60.6  
    60.7 -instance list :: (term) order
    60.8 +instance list :: (type) order
    60.9      (prefix_refl,prefix_trans,prefix_antisym,prefix_less_le)
   60.10  
   60.11  end
    61.1 --- a/src/HOL/UNITY/Simple/Reach.thy	Sat Dec 01 18:51:46 2001 +0100
    61.2 +++ b/src/HOL/UNITY/Simple/Reach.thy	Sat Dec 01 18:52:32 2001 +0100
    61.3 @@ -11,7 +11,7 @@
    61.4  types   vertex
    61.5          state = "vertex=>bool"
    61.6  
    61.7 -arities vertex :: term
    61.8 +arities vertex :: type
    61.9  
   61.10  consts
   61.11    init ::  "vertex"
    62.1 --- a/src/HOL/W0/Type.thy	Sat Dec 01 18:51:46 2001 +0100
    62.2 +++ b/src/HOL/W0/Type.thy	Sat Dec 01 18:52:32 2001 +0100
    62.3 @@ -10,7 +10,7 @@
    62.4  
    62.5  (* new class for structures containing type variables *)
    62.6  classes
    62.7 -        type_struct < term 
    62.8 +        type_struct < type
    62.9  
   62.10  (* type expressions *)
   62.11  datatype
   62.12 @@ -23,7 +23,7 @@
   62.13  arities
   62.14          typ::type_struct
   62.15          list::(type_struct)type_struct
   62.16 -        fun::(term,type_struct)type_struct
   62.17 +        fun::(type,type_struct)type_struct
   62.18  
   62.19  (* substitutions *)
   62.20  
    63.1 --- a/src/HOL/arith_data.ML	Sat Dec 01 18:51:46 2001 +0100
    63.2 +++ b/src/HOL/arith_data.ML	Sat Dec 01 18:52:32 2001 +0100
    63.3 @@ -138,8 +138,7 @@
    63.4  
    63.5  (** prepare nat_cancel simprocs **)
    63.6  
    63.7 -fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) 
    63.8 -                                (s, HOLogic.termT);
    63.9 +fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context ())) s;
   63.10  val prep_pats = map prep_pat;
   63.11  
   63.12  fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
    64.1 --- a/src/HOL/ex/MT.thy	Sat Dec 01 18:51:46 2001 +0100
    64.2 +++ b/src/HOL/ex/MT.thy	Sat Dec 01 18:52:32 2001 +0100
    64.3 @@ -31,19 +31,19 @@
    64.4    TyEnv
    64.5  
    64.6  arities 
    64.7 -  Const :: term
    64.8 +  Const :: type
    64.9  
   64.10 -  ExVar :: term
   64.11 -  Ex :: term
   64.12 +  ExVar :: type
   64.13 +  Ex :: type
   64.14  
   64.15 -  TyConst :: term
   64.16 -  Ty :: term
   64.17 +  TyConst :: type
   64.18 +  Ty :: type
   64.19  
   64.20 -  Clos :: term
   64.21 -  Val :: term
   64.22 +  Clos :: type
   64.23 +  Val :: type
   64.24  
   64.25 -  ValEnv :: term
   64.26 -  TyEnv :: term
   64.27 +  ValEnv :: type
   64.28 +  TyEnv :: type
   64.29  
   64.30  consts
   64.31    c_app :: [Const, Const] => Const
    65.1 --- a/src/HOL/ex/PER.thy	Sat Dec 01 18:51:46 2001 +0100
    65.2 +++ b/src/HOL/ex/PER.thy	Sat Dec 01 18:52:32 2001 +0100
    65.3 @@ -8,39 +8,40 @@
    65.4  theory PER = Main:
    65.5  
    65.6  text {*
    65.7 - Higher-order quotients are defined over partial equivalence relations
    65.8 - (PERs) instead of total ones.  We provide axiomatic type classes
    65.9 - @{text "equiv < partial_equiv"} and a type constructor
   65.10 - @{text "'a quot"} with basic operations.  This development is based
   65.11 - on:
   65.12 +  Higher-order quotients are defined over partial equivalence
   65.13 +  relations (PERs) instead of total ones.  We provide axiomatic type
   65.14 +  classes @{text "equiv < partial_equiv"} and a type constructor
   65.15 +  @{text "'a quot"} with basic operations.  This development is based
   65.16 +  on:
   65.17  
   65.18 - Oscar Slotosch: \emph{Higher Order Quotients and their Implementation
   65.19 - in Isabelle HOL.}  Elsa L. Gunter and Amy Felty, editors, Theorem
   65.20 - Proving in Higher Order Logics: TPHOLs '97, Springer LNCS 1275, 1997.
   65.21 +  Oscar Slotosch: \emph{Higher Order Quotients and their
   65.22 +  Implementation in Isabelle HOL.}  Elsa L. Gunter and Amy Felty,
   65.23 +  editors, Theorem Proving in Higher Order Logics: TPHOLs '97,
   65.24 +  Springer LNCS 1275, 1997.
   65.25  *}
   65.26  
   65.27  
   65.28  subsection {* Partial equivalence *}
   65.29  
   65.30  text {*
   65.31 - Type class @{text partial_equiv} models partial equivalence relations
   65.32 - (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation,
   65.33 - which is required to be symmetric and transitive, but not necessarily
   65.34 - reflexive.
   65.35 +  Type class @{text partial_equiv} models partial equivalence
   65.36 +  relations (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a =>
   65.37 +  bool"} relation, which is required to be symmetric and transitive,
   65.38 +  but not necessarily reflexive.
   65.39  *}
   65.40  
   65.41  consts
   65.42    eqv :: "'a => 'a => bool"    (infixl "\<sim>" 50)
   65.43  
   65.44 -axclass partial_equiv < "term"
   65.45 +axclass partial_equiv < type
   65.46    partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
   65.47    partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
   65.48  
   65.49  text {*
   65.50 - \medskip The domain of a partial equivalence relation is the set of
   65.51 - reflexive elements.  Due to symmetry and transitivity this
   65.52 - characterizes exactly those elements that are connected with
   65.53 - \emph{any} other one.
   65.54 +  \medskip The domain of a partial equivalence relation is the set of
   65.55 +  reflexive elements.  Due to symmetry and transitivity this
   65.56 +  characterizes exactly those elements that are connected with
   65.57 +  \emph{any} other one.
   65.58  *}
   65.59  
   65.60  constdefs
   65.61 @@ -64,9 +65,9 @@
   65.62  subsection {* Equivalence on function spaces *}
   65.63  
   65.64  text {*
   65.65 - The @{text \<sim>} relation is lifted to function spaces.  It is
   65.66 - important to note that this is \emph{not} the direct product, but a
   65.67 - structural one corresponding to the congruence property.
   65.68 +  The @{text \<sim>} relation is lifted to function spaces.  It is
   65.69 +  important to note that this is \emph{not} the direct product, but a
   65.70 +  structural one corresponding to the congruence property.
   65.71  *}
   65.72  
   65.73  defs (overloaded)
   65.74 @@ -81,8 +82,8 @@
   65.75    by (unfold eqv_fun_def) blast
   65.76  
   65.77  text {*
   65.78 - The class of partial equivalence relations is closed under function
   65.79 - spaces (in \emph{both} argument positions).
   65.80 +  The class of partial equivalence relations is closed under function
   65.81 +  spaces (in \emph{both} argument positions).
   65.82  *}
   65.83  
   65.84  instance fun :: (partial_equiv, partial_equiv) partial_equiv
   65.85 @@ -113,18 +114,18 @@
   65.86  subsection {* Total equivalence *}
   65.87  
   65.88  text {*
   65.89 - The class of total equivalence relations on top of PERs.  It
   65.90 - coincides with the standard notion of equivalence, i.e.\
   65.91 - @{text "\<sim> :: 'a => 'a => bool"} is required to be reflexive, transitive
   65.92 - and symmetric.
   65.93 +  The class of total equivalence relations on top of PERs.  It
   65.94 +  coincides with the standard notion of equivalence, i.e.\ @{text "\<sim>
   65.95 +  :: 'a => 'a => bool"} is required to be reflexive, transitive and
   65.96 +  symmetric.
   65.97  *}
   65.98  
   65.99  axclass equiv < partial_equiv
  65.100    eqv_refl [intro]: "x \<sim> x"
  65.101  
  65.102  text {*
  65.103 - On total equivalences all elements are reflexive, and congruence
  65.104 - holds unconditionally.
  65.105 +  On total equivalences all elements are reflexive, and congruence
  65.106 +  holds unconditionally.
  65.107  *}
  65.108  
  65.109  theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain"
  65.110 @@ -145,8 +146,8 @@
  65.111  subsection {* Quotient types *}
  65.112  
  65.113  text {*
  65.114 - The quotient type @{text "'a quot"} consists of all \emph{equivalence
  65.115 - classes} over elements of the base type @{typ 'a}.
  65.116 +  The quotient type @{text "'a quot"} consists of all
  65.117 +  \emph{equivalence classes} over elements of the base type @{typ 'a}.
  65.118  *}
  65.119  
  65.120  typedef 'a quot = "{{x. a \<sim> x}| a::'a. True}"
  65.121 @@ -159,8 +160,8 @@
  65.122    by (unfold quot_def) blast
  65.123  
  65.124  text {*
  65.125 - \medskip Abstracted equivalence classes are the canonical
  65.126 - representation of elements of a quotient type.
  65.127 +  \medskip Abstracted equivalence classes are the canonical
  65.128 +  representation of elements of a quotient type.
  65.129  *}
  65.130  
  65.131  constdefs
  65.132 @@ -183,8 +184,8 @@
  65.133  subsection {* Equality on quotients *}
  65.134  
  65.135  text {*
  65.136 - Equality of canonical quotient elements corresponds to the original
  65.137 - relation as follows.
  65.138 +  Equality of canonical quotient elements corresponds to the original
  65.139 +  relation as follows.
  65.140  *}
  65.141  
  65.142  theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
    66.1 --- a/src/HOL/hologic.ML	Sat Dec 01 18:51:46 2001 +0100
    66.2 +++ b/src/HOL/hologic.ML	Sat Dec 01 18:52:32 2001 +0100
    66.3 @@ -7,9 +7,9 @@
    66.4  
    66.5  signature HOLOGIC =
    66.6  sig
    66.7 -  val termC: class
    66.8 -  val termS: sort
    66.9 -  val termT: typ
   66.10 +  val typeS: sort
   66.11 +  val typeT: typ
   66.12 +  val read_cterm: Sign.sg -> string -> cterm
   66.13    val boolN: string
   66.14    val boolT: typ
   66.15    val false_const: term
   66.16 @@ -80,11 +80,12 @@
   66.17  structure HOLogic: HOLOGIC =
   66.18  struct
   66.19  
   66.20 -(* basics *)
   66.21 +(* HOL syntax *)
   66.22  
   66.23 -val termC: class = "term";
   66.24 -val termS: sort = [termC];
   66.25 -val termT = TypeInfer.anyT termS;
   66.26 +val typeS: sort = ["HOL.type"];
   66.27 +val typeT = TypeInfer.anyT typeS;
   66.28 +
   66.29 +fun read_cterm sg s = Thm.read_cterm sg (s, typeT);
   66.30  
   66.31  
   66.32  (* bool and set *)
    67.1 --- a/src/HOLCF/Discrete.ML	Sat Dec 01 18:51:46 2001 +0100
    67.2 +++ b/src/HOLCF/Discrete.ML	Sat Dec 01 18:52:32 2001 +0100
    67.3 @@ -10,11 +10,11 @@
    67.4  Addsimps [undiscr_Discr];
    67.5  
    67.6  Goal
    67.7 - "!!S::nat=>('a::term)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
    67.8 + "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
    67.9  by (fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
   67.10  qed "discr_chain_f_range0";
   67.11  
   67.12 -Goalw [cont,is_lub_def,is_ub_def] "cont(%x::('a::term)discr. f x)";
   67.13 +Goalw [cont,is_lub_def,is_ub_def] "cont(%x::('a::type)discr. f x)";
   67.14  by (simp_tac (simpset() addsimps [discr_chain_f_range0]) 1);
   67.15  qed "cont_discr";
   67.16  AddIffs [cont_discr];
    68.1 --- a/src/HOLCF/Discrete.thy	Sat Dec 01 18:51:46 2001 +0100
    68.2 +++ b/src/HOLCF/Discrete.thy	Sat Dec 01 18:52:32 2001 +0100
    68.3 @@ -8,10 +8,10 @@
    68.4  
    68.5  Discrete = Discrete1 +
    68.6  
    68.7 -instance discr :: (term)cpo   (discr_cpo)
    68.8 +instance discr :: (type)cpo   (discr_cpo)
    68.9  
   68.10  constdefs
   68.11 -   undiscr :: ('a::term)discr => 'a
   68.12 +   undiscr :: ('a::type)discr => 'a
   68.13    "undiscr x == (case x of Discr y => y)"
   68.14  
   68.15  end
    69.1 --- a/src/HOLCF/Discrete0.ML	Sat Dec 01 18:51:46 2001 +0100
    69.2 +++ b/src/HOLCF/Discrete0.ML	Sat Dec 01 18:52:32 2001 +0100
    69.3 @@ -6,17 +6,17 @@
    69.4  Proves that 'a discr is a po
    69.5  *)
    69.6  
    69.7 -Goalw [less_discr_def] "(x::('a::term)discr) << x";
    69.8 +Goalw [less_discr_def] "(x::('a::type)discr) << x";
    69.9  by (rtac refl 1);
   69.10  qed "less_discr_refl";
   69.11  
   69.12  Goalw [less_discr_def]
   69.13 -  "!!x. [| (x::('a::term)discr) << y; y << z |] ==> x <<  z";
   69.14 +  "!!x. [| (x::('a::type)discr) << y; y << z |] ==> x <<  z";
   69.15  by (etac trans 1);
   69.16  by (assume_tac 1);
   69.17  qed "less_discr_trans";
   69.18  
   69.19  Goalw [less_discr_def]
   69.20 -  "!!x. [| (x::('a::term)discr) << y; y << x |] ==> x=y";
   69.21 +  "!!x. [| (x::('a::type)discr) << y; y << x |] ==> x=y";
   69.22  by (assume_tac 1);
   69.23  qed "less_discr_antisym";
    70.1 --- a/src/HOLCF/Discrete0.thy	Sat Dec 01 18:51:46 2001 +0100
    70.2 +++ b/src/HOLCF/Discrete0.thy	Sat Dec 01 18:52:32 2001 +0100
    70.3 @@ -8,11 +8,11 @@
    70.4  
    70.5  Discrete0 = Cont + Datatype +
    70.6  
    70.7 -datatype 'a discr = Discr "'a :: term"
    70.8 +datatype 'a discr = Discr "'a :: type"
    70.9  
   70.10 -instance discr :: (term)sq_ord
   70.11 +instance discr :: (type) sq_ord
   70.12  
   70.13  defs
   70.14 -less_discr_def "((op <<)::('a::term)discr=>'a discr=>bool)  ==  op ="
   70.15 +less_discr_def "((op <<)::('a::type)discr=>'a discr=>bool)  ==  op ="
   70.16  
   70.17  end
    71.1 --- a/src/HOLCF/Discrete1.ML	Sat Dec 01 18:51:46 2001 +0100
    71.2 +++ b/src/HOLCF/Discrete1.ML	Sat Dec 01 18:52:32 2001 +0100
    71.3 @@ -6,13 +6,13 @@
    71.4  Proves that 'a discr is a cpo
    71.5  *)
    71.6  
    71.7 -Goalw [less_discr_def] "((x::('a::term)discr) << y) = (x=y)";
    71.8 +Goalw [less_discr_def] "((x::('a::type)discr) << y) = (x=y)";
    71.9  by (rtac refl 1);
   71.10  qed "discr_less_eq";
   71.11  AddIffs [discr_less_eq];
   71.12  
   71.13  Goalw [chain_def]
   71.14 - "!!S::nat=>('a::term)discr. chain S ==> S i = S 0";
   71.15 + "!!S::nat=>('a::type)discr. chain S ==> S i = S 0";
   71.16  by (induct_tac "i" 1);
   71.17  by (rtac refl 1);
   71.18  by (etac subst 1);
   71.19 @@ -21,12 +21,12 @@
   71.20  qed "discr_chain0";
   71.21  
   71.22  Goal
   71.23 - "!!S::nat=>('a::term)discr. chain(S) ==> range(S) = {S 0}";
   71.24 + "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}";
   71.25  by (fast_tac (claset() addEs [discr_chain0]) 1);
   71.26  qed "discr_chain_range0";
   71.27  Addsimps [discr_chain_range0];
   71.28  
   71.29  Goalw [is_lub_def,is_ub_def]
   71.30 - "!!S. chain S ==> ? x::('a::term)discr. range(S) <<| x";
   71.31 + "!!S. chain S ==> ? x::('a::type)discr. range(S) <<| x";
   71.32  by (Asm_simp_tac 1);
   71.33  qed "discr_cpo";
    72.1 --- a/src/HOLCF/Discrete1.thy	Sat Dec 01 18:51:46 2001 +0100
    72.2 +++ b/src/HOLCF/Discrete1.thy	Sat Dec 01 18:52:32 2001 +0100
    72.3 @@ -8,7 +8,7 @@
    72.4  
    72.5  Discrete1 = Discrete0 +
    72.6  
    72.7 -instance discr :: (term)po
    72.8 +instance discr :: (type) po
    72.9    (less_discr_refl,less_discr_trans,less_discr_antisym)
   72.10  
   72.11  end
    73.1 --- a/src/HOLCF/FOCUS/Buffer.thy	Sat Dec 01 18:51:46 2001 +0100
    73.2 +++ b/src/HOLCF/FOCUS/Buffer.thy	Sat Dec 01 18:52:32 2001 +0100
    73.3 @@ -21,7 +21,7 @@
    73.4  Buffer = FOCUS + 
    73.5  
    73.6  types   D
    73.7 -arities D::term
    73.8 +arities D :: type
    73.9  
   73.10  datatype
   73.11  
    74.1 --- a/src/HOLCF/FOCUS/Fstream.thy	Sat Dec 01 18:51:46 2001 +0100
    74.2 +++ b/src/HOLCF/FOCUS/Fstream.thy	Sat Dec 01 18:52:32 2001 +0100
    74.3 @@ -10,7 +10,7 @@
    74.4  
    74.5  Fstream = Stream + 
    74.6  
    74.7 -default term
    74.8 +default type
    74.9  
   74.10  types 'a fstream = ('a lift) stream
   74.11  
    75.1 --- a/src/HOLCF/Fun1.ML	Sat Dec 01 18:51:46 2001 +0100
    75.2 +++ b/src/HOLCF/Fun1.ML	Sat Dec 01 18:52:32 2001 +0100
    75.3 @@ -10,19 +10,19 @@
    75.4  (* less_fun is a partial order on 'a => 'b                                  *)
    75.5  (* ------------------------------------------------------------------------ *)
    75.6  
    75.7 -val prems = goalw thy [less_fun_def] "(f::'a::term =>'b::po) << f";
    75.8 +val prems = goalw thy [less_fun_def] "(f::'a::type =>'b::po) << f";
    75.9  by (fast_tac (HOL_cs addSIs [refl_less]) 1);
   75.10  qed "refl_less_fun";
   75.11  
   75.12  val prems = goalw Fun1.thy [less_fun_def] 
   75.13 -        "[|(f1::'a::term =>'b::po) << f2; f2 << f1|] ==> f1 = f2";
   75.14 +        "[|(f1::'a::type =>'b::po) << f2; f2 << f1|] ==> f1 = f2";
   75.15  by (cut_facts_tac prems 1);
   75.16  by (stac expand_fun_eq 1);
   75.17  by (fast_tac (HOL_cs addSIs [antisym_less]) 1);
   75.18  qed "antisym_less_fun";
   75.19  
   75.20  val prems = goalw Fun1.thy [less_fun_def] 
   75.21 -        "[|(f1::'a::term =>'b::po) << f2; f2 << f3 |] ==> f1 << f3";
   75.22 +        "[|(f1::'a::type =>'b::po) << f2; f2 << f3 |] ==> f1 << f3";
   75.23  by (cut_facts_tac prems 1);
   75.24  by (strip_tac 1);
   75.25  by (rtac trans_less 1);
    76.1 --- a/src/HOLCF/Fun1.thy	Sat Dec 01 18:51:46 2001 +0100
    76.2 +++ b/src/HOLCF/Fun1.thy	Sat Dec 01 18:52:32 2001 +0100
    76.3 @@ -13,7 +13,7 @@
    76.4  instance flat<chfin (flat_imp_chfin)
    76.5  
    76.6  (* to make << defineable: *)
    76.7 -instance fun  :: (term,sq_ord)sq_ord
    76.8 +instance fun  :: (type, sq_ord) sq_ord
    76.9  
   76.10  defs
   76.11    less_fun_def "(op <<) == (%f1 f2.!x. f1 x << f2 x)"  
    77.1 --- a/src/HOLCF/Fun2.ML	Sat Dec 01 18:51:46 2001 +0100
    77.2 +++ b/src/HOLCF/Fun2.ML	Sat Dec 01 18:52:32 2001 +0100
    77.3 @@ -2,8 +2,6 @@
    77.4      ID:         $Id$
    77.5      Author:     Franz Regensburger
    77.6      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    77.7 -
    77.8 -Class Instance =>::(term,po)po
    77.9  *)
   77.10  
   77.11  (* for compatibility with old HOLCF-Version *)
   77.12 @@ -13,7 +11,7 @@
   77.13  qed "inst_fun_po";
   77.14  
   77.15  (* ------------------------------------------------------------------------ *)
   77.16 -(* Type 'a::term => 'b::pcpo is pointed                                     *)
   77.17 +(* Type 'a::type => 'b::pcpo is pointed                                     *)
   77.18  (* ------------------------------------------------------------------------ *)
   77.19  
   77.20  Goal "(%z. UU) << x";
   77.21 @@ -48,7 +46,7 @@
   77.22  (* upper bounds of function chains yield upper bound in the po range        *)
   77.23  (* ------------------------------------------------------------------------ *)
   77.24  
   77.25 -Goal "range(S::nat=>('a::term => 'b::po)) <| u ==> range(%i. S i x) <| u(x)";
   77.26 +Goal "range(S::nat=>('a::type => 'b::po)) <| u ==> range(%i. S i x) <| u(x)";
   77.27  by (rtac ub_rangeI 1);
   77.28  by (dtac ub_rangeD 1);
   77.29  by (asm_full_simp_tac (simpset() addsimps [less_fun]) 1);
   77.30 @@ -56,10 +54,10 @@
   77.31  qed "ub2ub_fun";
   77.32  
   77.33  (* ------------------------------------------------------------------------ *)
   77.34 -(* Type 'a::term => 'b::pcpo is chain complete                              *)
   77.35 +(* Type 'a::type => 'b::pcpo is chain complete                              *)
   77.36  (* ------------------------------------------------------------------------ *)
   77.37  
   77.38 -Goal "chain(S::nat=>('a::term => 'b::cpo)) ==> \
   77.39 +Goal "chain(S::nat=>('a::type => 'b::cpo)) ==> \
   77.40  \        range(S) <<| (% x. lub(range(% i. S(i)(x))))";
   77.41  by (rtac is_lubI 1);
   77.42  by (rtac ub_rangeI 1);
   77.43 @@ -78,7 +76,7 @@
   77.44  bind_thm ("thelub_fun", lub_fun RS thelubI);
   77.45  (* chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
   77.46  
   77.47 -Goal "chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x";
   77.48 +Goal "chain(S::nat=>('a::type => 'b::cpo)) ==> ? x. range(S) <<| x";
   77.49  by (rtac exI 1);
   77.50  by (etac lub_fun 1);
   77.51  qed "cpo_fun";
    78.1 --- a/src/HOLCF/Fun2.thy	Sat Dec 01 18:51:46 2001 +0100
    78.2 +++ b/src/HOLCF/Fun2.thy	Sat Dec 01 18:52:32 2001 +0100
    78.3 @@ -2,15 +2,13 @@
    78.4      ID:         $Id$
    78.5      Author:     Franz Regensburger
    78.6      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    78.7 -
    78.8 -Class Instance =>::(term,po)po
    78.9  *)
   78.10  
   78.11  Fun2 = Fun1 + 
   78.12  
   78.13 -(* default class is still term !*)
   78.14 +(* default class is still type!*)
   78.15  
   78.16 -instance fun  :: (term,po)po (refl_less_fun,antisym_less_fun,trans_less_fun)
   78.17 +instance fun  :: (type, po) po (refl_less_fun,antisym_less_fun,trans_less_fun)
   78.18  
   78.19  end
   78.20  
    79.1 --- a/src/HOLCF/Fun3.thy	Sat Dec 01 18:51:46 2001 +0100
    79.2 +++ b/src/HOLCF/Fun3.thy	Sat Dec 01 18:52:32 2001 +0100
    79.3 @@ -8,10 +8,10 @@
    79.4  
    79.5  Fun3 = Fun2 +
    79.6  
    79.7 -(* default class is still term *)
    79.8 +(* default class is still type *)
    79.9  
   79.10 -instance fun  :: (term,cpo)cpo         (cpo_fun)
   79.11 -instance fun  :: (term,pcpo)pcpo       (least_fun)
   79.12 +instance fun  :: (type, cpo) cpo         (cpo_fun)
   79.13 +instance fun  :: (type, pcpo)pcpo       (least_fun)
   79.14  
   79.15  end
   79.16  
    80.1 --- a/src/HOLCF/IMP/Denotational.thy	Sat Dec 01 18:51:46 2001 +0100
    80.2 +++ b/src/HOLCF/IMP/Denotational.thy	Sat Dec 01 18:52:32 2001 +0100
    80.3 @@ -9,7 +9,7 @@
    80.4  Denotational = HOLCF + Natural +
    80.5  
    80.6  constdefs
    80.7 -   dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)"
    80.8 +   dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)"
    80.9    "dlift f == (LAM x. case x of UU => UU | Def(y) => f$(Discr y))"
   80.10  
   80.11  consts D :: "com => state discr -> state lift"
    81.1 --- a/src/HOLCF/IOA/NTP/Multiset.thy	Sat Dec 01 18:51:46 2001 +0100
    81.2 +++ b/src/HOLCF/IOA/NTP/Multiset.thy	Sat Dec 01 18:52:32 2001 +0100
    81.3 @@ -15,7 +15,7 @@
    81.4  
    81.5  arities
    81.6  
    81.7 -  multiset :: (term) term
    81.8 +  multiset :: (type) type
    81.9  
   81.10  consts
   81.11  
    82.1 --- a/src/HOLCF/IOA/Storage/Correctness.thy	Sat Dec 01 18:51:46 2001 +0100
    82.2 +++ b/src/HOLCF/IOA/Storage/Correctness.thy	Sat Dec 01 18:52:32 2001 +0100
    82.3 @@ -8,7 +8,7 @@
    82.4  
    82.5  Correctness = SimCorrectness + Spec + Impl + 
    82.6  
    82.7 -default term
    82.8 +default type
    82.9  
   82.10  consts
   82.11  
    83.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Sat Dec 01 18:51:46 2001 +0100
    83.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Sat Dec 01 18:52:32 2001 +0100
    83.3 @@ -9,7 +9,7 @@
    83.4  		       
    83.5  Abstraction = LiveIOA + 
    83.6  
    83.7 -default term
    83.8 +default type
    83.9  
   83.10  
   83.11  consts
    84.1 --- a/src/HOLCF/IOA/meta_theory/Automata.thy	Sat Dec 01 18:51:46 2001 +0100
    84.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Sat Dec 01 18:52:32 2001 +0100
    84.3 @@ -9,7 +9,7 @@
    84.4  		       
    84.5  Automata = Option + Asig + Inductive +
    84.6  
    84.7 -default term
    84.8 +default type
    84.9   
   84.10  types
   84.11     ('a,'s)transition       =    "'s * 'a * 's"
    85.1 --- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Sat Dec 01 18:51:46 2001 +0100
    85.2 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Sat Dec 01 18:52:32 2001 +0100
    85.3 @@ -8,7 +8,7 @@
    85.4    
    85.5  LiveIOA = TLS + 
    85.6  
    85.7 -default term
    85.8 +default type
    85.9  
   85.10  types
   85.11  
    86.1 --- a/src/HOLCF/IOA/meta_theory/Pred.thy	Sat Dec 01 18:51:46 2001 +0100
    86.2 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Sat Dec 01 18:52:32 2001 +0100
    86.3 @@ -8,7 +8,7 @@
    86.4  	       
    86.5  Pred = Main +
    86.6  
    86.7 -default term
    86.8 +default type
    86.9  
   86.10  types
   86.11  
    87.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.thy	Sat Dec 01 18:51:46 2001 +0100
    87.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy	Sat Dec 01 18:52:32 2001 +0100
    87.3 @@ -8,7 +8,7 @@
    87.4  
    87.5  RefMappings = Traces  +
    87.6  
    87.7 -default term
    87.8 +default type
    87.9  
   87.10  consts
   87.11  
    88.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Sat Dec 01 18:51:46 2001 +0100
    88.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Sat Dec 01 18:52:32 2001 +0100
    88.3 @@ -8,9 +8,9 @@
    88.4  
    88.5  Sequence = Seq + 
    88.6  
    88.7 -default term
    88.8 +default type
    88.9  
   88.10 -types 'a Seq = ('a::term lift)seq
   88.11 +types 'a Seq = ('a::type lift)seq
   88.12  
   88.13  consts
   88.14  
   88.15 @@ -89,5 +89,4 @@
   88.16  (* for test purposes should be deleted FIX !! *)
   88.17  adm_all    "adm f"
   88.18  
   88.19 -
   88.20 -end
   88.21 \ No newline at end of file
   88.22 +end
    89.1 --- a/src/HOLCF/IOA/meta_theory/Simulations.thy	Sat Dec 01 18:51:46 2001 +0100
    89.2 +++ b/src/HOLCF/IOA/meta_theory/Simulations.thy	Sat Dec 01 18:52:32 2001 +0100
    89.3 @@ -8,7 +8,7 @@
    89.4  
    89.5  Simulations = RefCorrectness  +
    89.6  
    89.7 -default term
    89.8 +default type
    89.9  
   89.10  consts
   89.11  
    90.1 --- a/src/HOLCF/IOA/meta_theory/TL.thy	Sat Dec 01 18:51:46 2001 +0100
    90.2 +++ b/src/HOLCF/IOA/meta_theory/TL.thy	Sat Dec 01 18:52:32 2001 +0100
    90.3 @@ -8,7 +8,7 @@
    90.4  	       
    90.5  TL = Pred + Sequence +  
    90.6  
    90.7 -default term
    90.8 +default type
    90.9  
   90.10  types
   90.11  
    91.1 --- a/src/HOLCF/IOA/meta_theory/TLS.thy	Sat Dec 01 18:51:46 2001 +0100
    91.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Sat Dec 01 18:52:32 2001 +0100
    91.3 @@ -9,7 +9,7 @@
    91.4  		       
    91.5  TLS = IOA + TL + 
    91.6  
    91.7 -default term
    91.8 +default type
    91.9  
   91.10  types
   91.11  
    92.1 --- a/src/HOLCF/IOA/meta_theory/Traces.thy	Sat Dec 01 18:51:46 2001 +0100
    92.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Sat Dec 01 18:52:32 2001 +0100
    92.3 @@ -9,7 +9,7 @@
    92.4  		       
    92.5  Traces = Sequence + Automata +
    92.6  
    92.7 -default term
    92.8 +default type
    92.9   
   92.10  types  
   92.11     ('a,'s)pairs            =    "('a * 's) Seq"
    93.1 --- a/src/HOLCF/Lift.thy	Sat Dec 01 18:51:46 2001 +0100
    93.2 +++ b/src/HOLCF/Lift.thy	Sat Dec 01 18:52:32 2001 +0100
    93.3 @@ -4,11 +4,11 @@
    93.4      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    93.5  *)
    93.6  
    93.7 -header {* Lifting types of class term to flat pcpo's *}
    93.8 +header {* Lifting types of class type to flat pcpo's *}
    93.9  
   93.10  theory Lift = Cprod3:
   93.11  
   93.12 -defaultsort "term"
   93.13 +defaultsort type
   93.14  
   93.15  
   93.16  typedef 'a lift = "UNIV :: 'a option set" ..
   93.17 @@ -19,12 +19,12 @@
   93.18    Def :: "'a => 'a lift"
   93.19    "Def x == Abs_lift (Some x)"
   93.20  
   93.21 -instance lift :: ("term") sq_ord ..
   93.22 +instance lift :: (type) sq_ord ..
   93.23  
   93.24  defs (overloaded)
   93.25    less_lift_def: "x << y == (x=y | x=Undef)"
   93.26  
   93.27 -instance lift :: ("term") po
   93.28 +instance lift :: (type) po
   93.29  proof
   93.30    fix x y z :: "'a lift"
   93.31    show "x << x" by (unfold less_lift_def) blast
   93.32 @@ -111,7 +111,7 @@
   93.33    apply (blast intro: lub_finch1)
   93.34    done
   93.35  
   93.36 -instance lift :: ("term") pcpo
   93.37 +instance lift :: (type) pcpo
   93.38    apply intro_classes
   93.39     apply (erule cpo_lift)
   93.40    apply (rule least_lift)
   93.41 @@ -153,7 +153,7 @@
   93.42  consts
   93.43   flift1      :: "('a => 'b::pcpo) => ('a lift -> 'b)"
   93.44   flift2      :: "('a => 'b)       => ('a lift -> 'b lift)"
   93.45 - liftpair    ::"'a::term lift * 'b::term lift => ('a * 'b) lift"
   93.46 + liftpair    ::"'a::type lift * 'b::type lift => ('a * 'b) lift"
   93.47  
   93.48  defs
   93.49   flift1_def:
   93.50 @@ -219,7 +219,7 @@
   93.51  
   93.52  subsection {* Lift is flat *}
   93.53  
   93.54 -instance lift :: ("term") flat
   93.55 +instance lift :: (type) flat
   93.56  proof
   93.57    show "ALL x y::'a lift. x << y --> x = UU | x = y"
   93.58      by (simp add: less_lift)
    94.1 --- a/src/HOLCF/Porder.thy	Sat Dec 01 18:51:46 2001 +0100
    94.2 +++ b/src/HOLCF/Porder.thy	Sat Dec 01 18:52:32 2001 +0100
    94.3 @@ -18,8 +18,7 @@
    94.4          finite_chain :: "(nat=>'a::po)=>bool"
    94.5  
    94.6  syntax
    94.7 -
    94.8 -  "@LUB"	:: "(('b::term) => 'a) => 'a"	(binder "LUB " 10)
    94.9 +  "@LUB"	:: "('b => 'a) => 'a"	(binder "LUB " 10)
   94.10  
   94.11  translations
   94.12  
    95.1 --- a/src/HOLCF/Porder0.thy	Sat Dec 01 18:51:46 2001 +0100
    95.2 +++ b/src/HOLCF/Porder0.thy	Sat Dec 01 18:52:32 2001 +0100
    95.3 @@ -9,7 +9,7 @@
    95.4  Porder0 = Main +
    95.5  
    95.6  	(* introduce a (syntactic) class for the constant << *)
    95.7 -axclass sq_ord<term
    95.8 +axclass sq_ord < type
    95.9  
   95.10  	(* characteristic constant << for po *)
   95.11  consts