--- a/src/HOL/Transitive_Closure.thy Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Transitive_Closure.thy Mon Sep 13 11:13:15 2010 +0200
@@ -82,7 +82,7 @@
subsection {* Reflexive-transitive closure *}
lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r \<union> Id)"
- by (auto simp add: ext_iff)
+ by (auto simp add: fun_eq_iff)
lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
-- {* @{text rtrancl} of @{text r} contains @{text r} *}
@@ -186,7 +186,7 @@
lemmas rtrancl_idemp [simp] = rtranclp_idemp [to_set]
lemma rtrancl_idemp_self_comp [simp]: "R^* O R^* = R^*"
- apply (rule set_ext)
+ apply (rule set_eqI)
apply (simp only: split_tupled_all)
apply (blast intro: rtrancl_trans)
done
@@ -487,7 +487,7 @@
lemmas trancl_converseD = tranclp_converseD [to_set]
lemma tranclp_converse: "(r^--1)^++ = (r^++)^--1"
- by (fastsimp simp add: ext_iff
+ by (fastsimp simp add: fun_eq_iff
intro!: tranclp_converseI dest!: tranclp_converseD)
lemmas trancl_converse = tranclp_converse [to_set]