1.1 --- a/src/HOL/Fun.thy Tue Sep 07 15:56:33 2010 -0700
1.2 +++ b/src/HOL/Fun.thy Wed Sep 08 10:45:55 2010 +0200
1.3 @@ -18,6 +18,8 @@
1.4 apply (simp (no_asm_simp))
1.5 done
1.6
1.7 +lemmas expand_fun_eq = ext_iff
1.8 +
1.9 lemma apply_inverse:
1.10 "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
1.11 by auto
2.1 --- a/src/HOL/Set.thy Tue Sep 07 15:56:33 2010 -0700
2.2 +++ b/src/HOL/Set.thy Wed Sep 08 10:45:55 2010 +0200
2.3 @@ -498,6 +498,8 @@
2.4 lemma set_ext_iff [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))"
2.5 by(auto intro:set_ext)
2.6
2.7 +lemmas expand_set_eq [no_atp] = set_ext_iff
2.8 +
2.9 lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
2.10 -- {* Anti-symmetry of the subset relation. *}
2.11 by (iprover intro: set_ext subsetD)