src/HOL/Fun.thy
 changeset 21327 2b3c41d02e87 parent 21210 c17fd2df4e9e child 21547 9c9fdf4c2949
```     1.1 --- a/src/HOL/Fun.thy	Mon Nov 13 15:43:03 2006 +0100
1.2 +++ b/src/HOL/Fun.thy	Mon Nov 13 15:43:04 2006 +0100
1.3 @@ -7,13 +7,9 @@
1.5
1.6  theory Fun
1.7 -imports Typedef
1.8 +imports Set
1.9  begin
1.10
1.11 -instance set :: (type) order
1.12 -  by (intro_classes,
1.13 -      (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+)
1.14 -
1.15  constdefs
1.16    fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"
1.17     "fun_upd f a b == % x. if x=a then b else f x"
1.18 @@ -77,10 +73,11 @@
1.19
1.20  text{*As a simplification rule, it replaces all function equalities by
1.21    first-order equalities.*}
1.22 -lemma expand_fun_eq: "(f = g) = (! x. f(x)=g(x))"
1.23 +lemma expand_fun_eq: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
1.24  apply (rule iffI)
1.25  apply (simp (no_asm_simp))
1.26 -apply (rule ext, simp (no_asm_simp))
1.27 +apply (rule ext)
1.28 +apply (simp (no_asm_simp))
1.29  done
1.30
1.31  lemma apply_inverse:
```