# HG changeset patch
# User haftmann
# Date 1255088434 -7200
# Node ID 5564af2d0588a46882f0a3d6a78c8a9c41b56947
# Parent  dc883c6126d4474d3e924cef3294d2ab0d291c4c
simplified proof

diff -r dc883c6126d4 -r 5564af2d0588 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Fri Oct 09 13:34:40 2009 +0200
+++ b/src/HOL/Transitive_Closure.thy	Fri Oct 09 13:40:34 2009 +0200
@@ -77,7 +77,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 (simp add: mem_def pair_in_Id_conv [simplified mem_def] sup_fun_eq sup_bool_eq)
+  by (auto simp add: expand_fun_eq)
 
 lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
   -- {* @{text rtrancl} of @{text r} contains @{text r} *}