simplified proof
authorhaftmann
Fri Oct 09 13:40:34 2009 +0200 (2009-10-09)
changeset 329015564af2d0588
parent 32900 dc883c6126d4
child 32902 fbccf4522e14
child 32990 717680b14041
simplified proof
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Transitive_Closure.thy	Fri Oct 09 13:34:40 2009 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Oct 09 13:40:34 2009 +0200
     1.3 @@ -77,7 +77,7 @@
     1.4  subsection {* Reflexive-transitive closure *}
     1.5  
     1.6  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)"
     1.7 -  by (simp add: mem_def pair_in_Id_conv [simplified mem_def] sup_fun_eq sup_bool_eq)
     1.8 +  by (auto simp add: expand_fun_eq)
     1.9  
    1.10  lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
    1.11    -- {* @{text rtrancl} of @{text r} contains @{text r} *}