--- a/QuotMain.thy	Sat Nov 28 03:07:38 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 03:17:22 2009 +0100
@@ -1018,6 +1018,13 @@
 end 
 *}
 
+(* Rewrites the term with LAMBDA_PRS thm.
+
+Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))
+    with: f
+
+It proves the QUOTIENT assumptions by calling quotient_tac
+ *)
 ML {*
 fun lambda_prs_conv1 ctxt quot_thms ctrm =
   case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>