diff -r 017cb46b27bb -r 433f7c17255f Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Wed Jan 13 00:46:31 2010 +0100
+++ b/Quot/quotient_def.ML	Wed Jan 13 09:19:20 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