--- a/src/HOL/Transitive_Closure.thy Tue Oct 06 15:51:34 2009 +0200
+++ b/src/HOL/Transitive_Closure.thy Tue Oct 06 18:44:06 2009 +0200
@@ -76,8 +76,8 @@
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 Un Id)"
- by (simp add: expand_fun_eq sup2_iff)
+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 (simp add: mem_def pair_in_Id_conv [simplified mem_def] sup_fun_eq sup_bool_eq)
lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
-- {* @{text rtrancl} of @{text r} contains @{text r} *}