src/HOL/Transitive_Closure.thy
changeset 39198 f967a16dfcdd
parent 37677 c5a8b612e571
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Transitive_Closure.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -82,7 +82,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 (auto simp add: expand_fun_eq)
     1.8 +  by (auto simp add: ext_iff)
     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} *}
    1.12 @@ -487,7 +487,7 @@
    1.13  lemmas trancl_converseD = tranclp_converseD [to_set]
    1.14  
    1.15  lemma tranclp_converse: "(r^--1)^++ = (r^++)^--1"
    1.16 -  by (fastsimp simp add: expand_fun_eq
    1.17 +  by (fastsimp simp add: ext_iff
    1.18      intro!: tranclp_converseI dest!: tranclp_converseD)
    1.19  
    1.20  lemmas trancl_converse = tranclp_converse [to_set]