QuotScript.thy
changeset 416 3f3927f793d4
parent 396 7a1ab11ab023
child 427 5a3965aa4d80
--- a/QuotScript.thy	Fri Nov 27 07:16:16 2009 +0100
+++ b/QuotScript.thy	Fri Nov 27 08:15:23 2009 +0100
@@ -20,8 +20,8 @@
 by (blast)
 
 lemma EQUIV_REFL:
-  shows "EQUIV E ==> REFL E"
-  by (simp add: EQUIV_REFL_SYM_TRANS)
+  shows "EQUIV E \<Longrightarrow> (\<And>x. E x x)"
+  by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
 
 definition
   "PART_EQUIV 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)))"