--- a/ProgTutorial/Essential.thy	Tue Jun 01 00:07:47 2010 +0200
+++ b/ProgTutorial/Essential.thy	Tue Jun 01 00:26:48 2010 +0200
@@ -1295,27 +1295,30 @@
 
 text {*
   Type classes are formal names in the type system which are linked to
-  predicates on of one type variable (via the axclass mechanism) and thereby
-  express extra properties on types to be propagated by the type system.
+  predicates of one type variable (via the axclass mechanism) and thereby
+  express extra properties on types, to be propagated by the type system.
   The type-in-class judgement is defined
-  over a simple logic based on implication and schematic quantification.
-  The signature of this logic is called an order-sorted algebra (see Schmidt-Schauss)
-  and consists of an acyclic subclass relation and a set of image
+  via a simple logic over types, with inferences solely based on
+  modus ponens, instantiation and axiom use.
+  The declared axioms of this logic are called an order-sorted algebra (see Schmidt-Schauss).
+  It consists of an acyclic subclass relation and a set of image containment
   declarations for type constructors, called arities.
 
   A well-behaved high-level view on type classes has long been established
-  (cite Haftmann-Wenzel): the predicate behind a type class is the basis for a locale
-  (for context-management reasons)
-  and may use so-called type class parameters which are implemented as overloaded
-  constants. Overloading a constant means specifying its type-indexed value based on
-  a well-founded reduction towards other constants. When instantiating type classes
+  (cite Haftmann-Wenzel): the predicate behind a type class is the foundation
+  of a locale (for context-management reasons)
+  and may use so-called type class parameters. These are type-indexed constants
+  dependent on the sole type variable and are implemented via overloading.
+  Overloading a constant means specifying its value on a type based on
+  a well-founded reduction towards other values of constants on types.
+  When instantiating type classes
   (i.e. proving arities) you are specifying overloading via primitive recursion.
 
   Sorts are finite intersections of type classes and are implemented as lists
   of type class names. The empty intersection, i.e. the empty list, is therefore
   inhabited by all types and is called the topsort.
 
-  Free and schematic type variables may be annotated with sorts, thereby restricting
+  Free and schematic type variables are always annotated with sorts, thereby restricting
   the domain of types they quantify over and corresponding to an implicit hypothesis
   about the type variable.
 *}
@@ -1330,7 +1333,7 @@
   @{ML_file "Pure/sorts.ML"} contains comparison and normalization functionality for sorts,
     manages the order sorted algebra and offers an interface for reinterpreting
     derivations of type in class judgements
-  @{ML_file "Pure/defs.ML"} manages the constant definition dependency graph and keeps it well-founded
+  @{ML_file "Pure/defs.ML"} manages the constant dependency graph and keeps it well-founded
     (its define function doesn't terminate for complex non-well-founded dependencies)
   @{ML_file "Pure/axclass.ML"} manages the theorems that back up subclass and arity relations
     and provides basic infrastructure for establishing the high-level view on type classes

Binary file progtutorial.pdf has changed