diff -r fa2b4b7af755 -r 3c6f8a4074c4 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Tue Jan 12 16:12:54 2010 +0100
+++ b/Quot/quotient_def.ML	Tue Jan 12 16:21:42 2010 +0100
@@ -24,17 +24,17 @@
 end
 
 
-(* interface and syntax setup *)
+(** interface and syntax setup **)
+
+(* the ML-interface takes
 
-(* the ML-interface takes a 4-tuple consisting of     *)
-(*                                                    *)
-(* - the mixfix annotation                            *)
-(* - name and attributes                              *)
-(* - the new constant as term                         *)
-(* - the rhs of the definition as term                *)
-(*                                                    *)
-(* it returns the defined constant and its definition *)
-(* theorem; stores the data in the qconsts slot       *)
+ - the mixfix annotation
+ - name and attributes
+ - the new constant as term
+ - the rhs of the definition as term
+
+ it returns the defined constant and its definition
+ theorem; stores the data in the qconsts slot       *)
 
 fun quotient_def mx attr lhs rhs lthy =
 let