# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1263309702 -3600
# Node ID 3c6f8a4074c4b39b149dfd2787d197b0952c781c
# Parent  fa2b4b7af7557c564817e8da63275b3631006663
minor comment editing

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
diff -r fa2b4b7af755 -r 3c6f8a4074c4 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Tue Jan 12 16:12:54 2010 +0100
+++ b/Quot/quotient_info.ML	Tue Jan 12 16:21:42 2010 +0100
@@ -65,9 +65,8 @@
 
 exception NotFound
 
-(*******************)
-(* data containers *)
-(*******************)
+
+(** data containers **)
 
 (* info about map- and rel-functions for a type *)
 type maps_info = {mapfun: string, relmap: string}