--- a/LFex.thy	Fri Dec 04 16:40:23 2009 +0100
+++ b/LFex.thy	Fri Dec 04 16:53:11 2009 +0100
@@ -219,9 +219,7 @@
 ML {*
   val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM}
   val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps}
-  (*val trans2 = map (fn x => @{thm EQUALS_PRS} OF [x]) quot*)
-  val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quot
-  val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
+  val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quot
 *}
 
 lemma 

--- a/QuotList.thy	Fri Dec 04 16:40:23 2009 +0100
+++ b/QuotList.thy	Fri Dec 04 16:53:11 2009 +0100
@@ -52,7 +52,7 @@
   apply(induct_tac a)
   apply(simp)
   apply(simp)
-  apply(simp add: Quotient_REP_reflp[OF q])
+  apply(simp add: Quotient_rep_reflp[OF q])
   apply(rule allI)+
   apply(rule list_rel_rel[OF q])
   done
@@ -114,11 +114,11 @@
 
 (* TODO: Rest are unused *)
 
-lemma LIST_map_id:
+lemma list_map_id:
   shows "map (\<lambda>x. x) = (\<lambda>x. x)"
   by simp
 
-lemma list_rel_EQ:
+lemma list_rel_eq:
   shows "list_rel (op =) \<equiv> (op =)"
 apply(rule eq_reflection)
 unfolding expand_fun_eq
@@ -127,10 +127,9 @@
 apply(simp_all)
 done
 
-lemma list_rel_REFL:
+lemma list_rel_refl:
   assumes a: "\<And>x y. R x y = (R x = R y)"
   shows "list_rel R x x"
 by (induct x) (auto simp add: a)
 
-
 end

--- a/QuotMain.thy	Fri Dec 04 16:40:23 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 16:53:11 2009 +0100
@@ -1062,7 +1062,7 @@
  - Rewriting with definitions from the argument defs
      NewConst  ---->  (rep ---> abs) oldConst
 
- - Quotient_REL_REP:
+ - Quotient_rel_rep:
      Rel (Rep x) (Rep y)  ---->  x = y
 
  - ABS_REP
@@ -1082,11 +1082,9 @@
     val quotients = quotient_rules_get lthy
     val defs = map (Thm.varifyT o #def) (qconsts_dest thy);
     val absrep = map (fn x => @{thm Quotient_abs_rep} OF [x]) quotients
-    val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep;
-    val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quotients
-    val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
+    val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quotients
     val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps
-      (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)
+      (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ absrep @ reps_same @ defs)
   in
     EVERY' [
       (* (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))  ---->  f *)

--- a/QuotScript.thy	Fri Dec 04 16:40:23 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 16:53:11 2009 +0100
@@ -28,12 +28,12 @@
   by (simp add: equivp_reflp_symp_transp reflp_def)
 
 definition
-  "PART_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
+  "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
 
-lemma equivp_IMP_PART_equivp:
+lemma equivp_IMP_part_equivp:
   assumes a: "equivp E"
-  shows "PART_equivp E"
-using a unfolding equivp_def PART_equivp_def
+  shows "part_equivp E"
+using a unfolding equivp_def part_equivp_def
 by auto
 
 definition
@@ -47,9 +47,9 @@
 using a unfolding Quotient_def
 by simp
 
-lemma Quotient_REP_reflp:
+lemma Quotient_rep_reflp:
   assumes a: "Quotient E Abs Rep"
-  shows "E (Rep a) (Rep a)" 
+  shows "E (Rep a) (Rep a)"
 using a unfolding Quotient_def
 by blast
 
@@ -59,21 +59,10 @@
 using a unfolding Quotient_def
 by blast
 
-lemma Quotient_REL_ABS:
-  assumes a: "Quotient E Abs Rep"
-  shows "E r s \<Longrightarrow> Abs r = Abs s"
-using a unfolding Quotient_def
-by blast
-
-lemma Quotient_REL_ABS_EQ:
-  assumes a: "Quotient E Abs Rep"
-  shows "E r r \<Longrightarrow> E s s \<Longrightarrow> E r s = (Abs r = Abs s)"
-using a unfolding Quotient_def
-by blast
-
-lemma Quotient_REL_REP:
+lemma Quotient_rel_rep:
   assumes a: "Quotient R Abs Rep"
-  shows "R (Rep a) (Rep b) = (a = b)"
+  shows "R (Rep a) (Rep b) \<equiv> (a = b)"
+apply (rule eq_reflection)
 using a unfolding Quotient_def
 by metis
 
@@ -251,7 +240,7 @@
 apply(metis fun_rel_IMP)
 using r1 unfolding Respects_def expand_fun_eq
 apply(simp (no_asm_use))
-apply(metis Quotient_rel[OF q2] Quotient_REL_REP[OF q1])
+apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1])
 done
 
 (* ask Peter: fun_rel_IMP used twice *) 
@@ -265,12 +254,6 @@
 using q1 q2 r1 r2 a
 by (simp add: fun_rel_EQUALS)
 
-(* We don't use it, it is exactly the same as Quotient_REL_REP but wrong way *)
-lemma EQUALS_PRS:
-  assumes q: "Quotient R Abs Rep"
-  shows "(x = y) = R (Rep x) (Rep y)"
-by (rule Quotient_REL_REP[OF q, symmetric])
-
 lemma equals_rsp:
   assumes q: "Quotient R Abs Rep"
   and     a: "R xa xb" "R ya yb"
@@ -328,14 +311,14 @@
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
   shows "R x1 (Rep (Abs x2))"
-using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_REP_reflp[OF q])
+using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
 
 (* Not used *)
 lemma REP_ABS_RSP_LEFT:
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
   shows "R x1 (Rep (Abs x2))"
-using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_REP_reflp[OF q])
+using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
 
 (* ----------------------------------------------------- *)
 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE,           *)
@@ -567,5 +550,21 @@
   using a unfolding Quotient_def
   by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply)
 
+
+(* UNUSED *)
+lemma Quotient_rel_abs:
+  assumes a: "Quotient E Abs Rep"
+  shows "E r s \<Longrightarrow> Abs r = Abs s"
+using a unfolding Quotient_def
+by blast
+
+lemma Quotient_rel_abs_eq:
+  assumes a: "Quotient E Abs Rep"
+  shows "E r r \<Longrightarrow> E s s \<Longrightarrow> E r s = (Abs r = Abs s)"
+using a unfolding Quotient_def
+by blast
+
+
+
 end