tuned;
authorwenzelm
Tue, 02 May 2006 00:33:40 +0200
changeset 19531 89970e06351f
parent 19530 486dd4b07188
child 19532 dae447f2b0b4
tuned;
src/Pure/axclass.ML
src/Pure/sorts.ML
--- a/src/Pure/axclass.ML	Tue May 02 00:20:40 2006 +0200
+++ b/src/Pure/axclass.ML	Tue May 02 00:33:40 2006 +0200
@@ -349,6 +349,7 @@
 end;
 
 
+
 (** axiomatizations **)
 
 local
--- a/src/Pure/sorts.ML	Tue May 02 00:20:40 2006 +0200
+++ b/src/Pure/sorts.ML	Tue May 02 00:33:40 2006 +0200
@@ -90,11 +90,11 @@
     subclass relation, which needs to be transitive and acyclic.
 
   arities: table of association lists of all type arities; (t, ars)
-    means that type constructor t has the arities ars; an element (c,
-    (c0, Ss)) of ars represents the arity t::(Ss)c being derived via
-    c0 < c.  "Coregularity" of the arities structure requires that for
-    any two declarations t::(Ss1)c1 and t::(Ss2)c2 such that c1 <= c2
-    holds Ss1 <= Ss2.
+    means that type constructor t has the arities ars; an element
+    (c, (c0, Ss)) of ars represents the arity t::(Ss)c being derived
+    via c0 <= c.  "Coregularity" of the arities structure requires
+    that for any two declarations t::(Ss1)c1 and t::(Ss2)c2 such that
+    c1 <= c2 holds Ss1 <= Ss2.
 *)
 
 type classes = stamp Graph.T;