--- a/QuotMain.thy	Mon Nov 30 02:05:22 2009 +0100
+++ b/QuotMain.thy	Mon Nov 30 10:16:10 2009 +0100
@@ -1102,6 +1102,25 @@
           Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
 *}
 
+(*
+ Cleaning the theorem consists of 5 kinds of rewrites.
+ These rewrites can be done independently and in any order.
+
+ - LAMBDA_PRS:
+     (Rep1 ---> Abs2) (\<lambda>x. Rep2 (?f (Abs1 x)))       \<equiv>   ?f
+ - Rewriting with definitions from the argument defs
+     (Abs) OldConst (Rep Args)                       \<equiv>   NewConst Args
+ - QUOTIENT_REL_REP:
+     Rel (Rep x) (Rep y)                             \<equiv>   x = y
+ - FORALL_PRS (and the same for exists: EXISTS_PRS)
+     \<forall>x\<in>Respects R. (abs ---> id) ?f                 \<equiv>   \<forall>x. ?f
+ - applic_prs
+     Abs1 ((Abs2 --> Rep1) f (Rep2 args))            \<equiv>   f args
+
+ The first one is implemented as a conversion (fast).
+ The second and third one are a simp_tac (fast).
+ The last two are EqSubst (slow).
+*)
 ML {*
 fun clean_tac lthy quot defs aps =
   let