diff -r 7be9b054f672 -r c46b6abad24b Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Sun Jan 24 23:41:27 2010 +0100
+++ b/Quot/QuotScript.thy	Mon Jan 25 17:53:08 2010 +0100
@@ -36,6 +36,10 @@
   shows "equivp R"
   using assms by (simp add: equivp_reflp_symp_transp)
 
+lemma eq_imp_rel:  
+  shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" 
+by (simp add: equivp_reflp)
+
 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)))"
 
@@ -380,10 +384,10 @@
 apply rule+
 apply (erule_tac x="xb" in ballE)
 prefer 2
-apply (metis in_respects)
+apply (metis)
 apply (erule_tac x="ya" in ballE)
 prefer 2
-apply (metis in_respects)
+apply (metis)
 apply (metis in_respects)
 apply (erule conjE)+
 apply (erule bexE)
@@ -394,10 +398,10 @@
 apply rule+
 apply (erule_tac x="xb" in ballE)
 prefer 2
-apply (metis in_respects)
+apply (metis)
 apply (erule_tac x="ya" in ballE)
 prefer 2
-apply (metis in_respects)
+apply (metis)
 apply (metis in_respects)
 done