changeset 39443 | 297cd703f1f0 |
parent 39428 | f967a16dfcdd |
child 39535 | d7728f65b353 |
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