# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259374642 -3600
# Node ID 98936120ab02a2c02590fe500400e76e7c0c5287
# Parent  12fc780ff0e8fff594fed6678ebd7d620140093b
Merged comment

diff -r 12fc780ff0e8 -r 98936120ab02 QuotMain.thy
--- 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 _)) =>