diff -r 8ba35ce16f7e -r 67739818af3f Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Wed Jan 27 14:56:58 2010 +0100
+++ b/Quot/quotient_tacs.ML	Wed Jan 27 14:57:11 2010 +0100
@@ -520,9 +520,12 @@
 
       - Quotient_abs_rep Quotient_rel_rep 
         babs_prs all_prs ex_prs ex1_prs
-      - id_simps
-     
-     and folding of definitions and preservation lemmas
+
+      - id_simps and preservation lemmas and 
+
+      - symmetric versions of the definitions    
+        (that is definitions of quotient constants 
+         are folded)
 
   4. test for refl
 *)