--- a/Quot/QuotMain.thy	Thu Dec 10 08:55:30 2009 +0100
+++ b/Quot/QuotMain.thy	Thu Dec 10 10:21:51 2009 +0100
@@ -84,57 +84,6 @@
 apply(simp add: equivp[simplified equivp_def])
 done
 
-lemma R_trans:
-  assumes ab: "R a b"
-  and     bc: "R b c"
-  shows "R a c"
-proof -
-  have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp
-  moreover have ab: "R a b" by fact
-  moreover have bc: "R b c" by fact
-  ultimately show "R a c" unfolding transp_def by blast
-qed
-
-lemma R_sym:
-  assumes ab: "R a b"
-  shows "R b a"
-proof -
-  have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp
-  then show "R b a" using ab unfolding symp_def by blast
-qed
-
-lemma R_trans2:
-  assumes ac: "R a c"
-  and     bd: "R b d"
-  shows "R a b = R c d"
-using ac bd
-by (blast intro: R_trans R_sym)
-
-lemma REPS_same:
-  shows "R (REP a) (REP b) \<equiv> (a = b)"
-proof -
-  have "R (REP a) (REP b) = (a = b)"
-  proof
-    assume as: "R (REP a) (REP b)"
-    from rep_prop
-    obtain x y
-      where eqs: "Rep a = R x" "Rep b = R y" by blast
-    from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
-    then have "R x (Eps (R y))" using lem9 by simp
-    then have "R (Eps (R y)) x" using R_sym by blast
-    then have "R y x" using lem9 by simp
-    then have "R x y" using R_sym by blast
-    then have "ABS x = ABS y" using thm11 by simp
-    then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
-    then show "a = b" using rep_inverse by simp
-  next
-    assume ab: "a = b"
-    have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp
-    then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto
-  qed
-  then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
-qed
-
 end
 
 section {* type definition for the quotient type *}

--- a/UnusedQuotMain.thy	Thu Dec 10 08:55:30 2009 +0100
+++ b/UnusedQuotMain.thy	Thu Dec 10 10:21:51 2009 +0100
@@ -628,3 +628,60 @@
   |> cprop_of |> Thm.dest_equals |> snd
 
 *}
+
+(* Unused part of the locale *)
+
+lemma R_trans:
+  assumes ab: "R a b"
+  and     bc: "R b c"
+  shows "R a c"
+proof -
+  have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp
+  moreover have ab: "R a b" by fact
+  moreover have bc: "R b c" by fact
+  ultimately show "R a c" unfolding transp_def by blast
+qed
+
+lemma R_sym:
+  assumes ab: "R a b"
+  shows "R b a"
+proof -
+  have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp
+  then show "R b a" using ab unfolding symp_def by blast
+qed
+
+lemma R_trans2:
+  assumes ac: "R a c"
+  and     bd: "R b d"
+  shows "R a b = R c d"
+using ac bd
+by (blast intro: R_trans R_sym)
+
+lemma REPS_same:
+  shows "R (REP a) (REP b) \<equiv> (a = b)"
+proof -
+  have "R (REP a) (REP b) = (a = b)"
+  proof
+    assume as: "R (REP a) (REP b)"
+    from rep_prop
+    obtain x y
+      where eqs: "Rep a = R x" "Rep b = R y" by blast
+    from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
+    then have "R x (Eps (R y))" using lem9 by simp
+    then have "R (Eps (R y)) x" using R_sym by blast
+    then have "R y x" using lem9 by simp
+    then have "R x y" using R_sym by blast
+    then have "ABS x = ABS y" using thm11 by simp
+    then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
+    then show "a = b" using rep_inverse by simp
+  next
+    assume ab: "a = b"
+    have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp
+    then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto
+  qed
+  then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
+qed
+
+
+
+