quotient.ML
changeset 329 5d06e1dba69a
parent 321 f46dc0ca08c3
child 331 345c422b1cb5
--- a/quotient.ML	Sat Nov 21 14:45:25 2009 +0100
+++ b/quotient.ML	Sat Nov 21 23:23:01 2009 +0100
@@ -39,8 +39,8 @@
 end
 
 
-(* definition of the quotient type *)
-(***********************************)
+(* definition of quotient types *)
+(********************************)
 
 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
 fun typedef_term rel rty lthy =