src/HOL/Fun.thy

--- a/src/HOL/Fun.thy	Tue Sep 07 15:56:33 2010 -0700
+++ b/src/HOL/Fun.thy	Wed Sep 08 10:45:55 2010 +0200
@@ -18,6 +18,8 @@
 apply (simp (no_asm_simp))
 done
 
+lemmas expand_fun_eq = ext_iff
+
 lemma apply_inverse:
   "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
   by auto