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)))"