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.4  header {* Notions about functions *}
     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: