# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259592022 -3600
# Node ID ce1f8a28492011e99dd1f73ff1a5d827b84b045c
# Parent  a0ddf16f05f579d1a9a93055e00b1c88be7a8cca
merge

diff -r a0ddf16f05f5 -r ce1f8a284920 QuotMain.thy
--- a/QuotMain.thy	Mon Nov 30 15:36:49 2009 +0100
+++ b/QuotMain.thy	Mon Nov 30 15:40:22 2009 +0100
@@ -1066,24 +1066,24 @@
 *}
 
 (*
- TODO: Update
- Cleaning the theorem consists of 5 kinds of rewrites.
- These rewrites can be done independently and in any order.
+ Cleaning the theorem consists of 6 kinds of rewrites.
+ The first two need to be done before fun_map is unfolded
 
  - LAMBDA_PRS:
-     (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))        ---->   f
+     (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))       \<Longrightarrow>   f
+ - FORALL_PRS (and the same for exists: EXISTS_PRS)
+     \<forall>x\<in>Respects R. (abs ---> id) ?f                \<Longrightarrow>   \<forall>x. ?f
  - Rewriting with definitions from the argument defs
-     (Abs) OldConst (Rep Args)                       ---->   NewConst Args
+     NewConst                                       \<Longrightarrow>   (rep ---> abs) oldConst
  - QUOTIENT_REL_REP:
-     Rel (Rep x) (Rep y)                             ---->   x = y
- - FORALL_PRS (and the same for exists: EXISTS_PRS)
-     \<forall>x\<in>Respects R. (abs ---> id) f                  ---->   \<forall>x. f
- - applic_prs
-     Abs1 ((Abs2 --> Rep1) f (Rep2 args))            ---->   f args
+     Rel (Rep x) (Rep y)                            \<Longrightarrow>   x = y
+ - ABS_REP
+     Abs (Rep x)                                    \<Longrightarrow>   x
+ - id_simps; fun_map.simps
 
  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).
+ The second one is an EqSubst (slow).
+ The rest are a simp_tac and are fast.
 *)
 ML {*
 fun clean_tac lthy quot defs aps =