--- a/ProgTutorial/Essential.thy	Mon May 31 23:29:06 2010 +0200
+++ b/ProgTutorial/Essential.thy	Tue Jun 01 00:07:47 2010 +0200
@@ -1294,9 +1294,30 @@
 section {* Sorts (TBD) *}
 
 text {*
-  Free and schematic variables may be annotated with sorts. Sorts are lists
-  of strings, whereby each string stands for a class. Sorts classify types.
-
+  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.
+  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
+  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
+  (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
+  the domain of types they quantify over and corresponding to an implicit hypothesis
+  about the type variable.
 *}
 
 
@@ -1306,9 +1327,18 @@
   \begin{readmore}
   Classes, sorts and arities are defined in @{ML_file "Pure/term.ML"}.
   
-  @{ML_file "Pure/sign.ML"}
-  @{ML_file "Pure/sorts.ML"}
-  @{ML_file "Pure/axclass.ML"}
+  @{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
+    (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
+  @{ML_file "Pure/sign.ML"} is a common interface to all the type-theory-like declarations
+    (especially names, constants, paths, type classes) a
+    theory acquires by theory extension mechanisms and manages associated certification
+    functionality.
+    It also provides the most needed functionality from individual underlying modules.
   \end{readmore}
 *}
 

Binary file progtutorial.pdf has changed