src/HOL/HOL.thy
changeset 44277 bcb696533579
parent 44121 44adaa6db327
child 44921 58eef4843641
     1.1 --- a/src/HOL/HOL.thy	Thu Aug 18 13:10:24 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Aug 18 13:25:17 2011 +0200
     1.3 @@ -1394,6 +1394,11 @@
     1.4    "f (if c then x else y) = (if c then f x else f y)"
     1.5    by simp
     1.6  
     1.7 +text{*As a simplification rule, it replaces all function equalities by
     1.8 +  first-order equalities.*}
     1.9 +lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
    1.10 +  by auto
    1.11 +
    1.12  
    1.13  subsubsection {* Generic cases and induction *}
    1.14