added eta_contract_eq, also to simpset
authoroheimb
Fri Jun 02 17:47:41 2000 +0200 (2000-06-02)
changeset 902309d02e7365c1
parent 9022 a389be05c06f
child 9024 b1f37f6819c4
added eta_contract_eq, also to simpset
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Fri Jun 02 17:47:03 2000 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Fri Jun 02 17:47:41 2000 +0200
     1.3 @@ -62,6 +62,10 @@
     1.4  by (rtac refl 1);
     1.5  qed "meta_eq_to_obj_eq";
     1.6  
     1.7 +Goal "(%s. f s) = f";
     1.8 +br refl 1;
     1.9 +qed "eta_contract_eq";
    1.10 +
    1.11  local
    1.12  
    1.13    fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]);
    1.14 @@ -437,6 +441,7 @@
    1.15      HOL_basic_ss addsimps 
    1.16       ([triv_forall_equality, (* prunes params *)
    1.17         True_implies_equals, (* prune asms `True' *)
    1.18 +       eta_contract_eq, (* prunes eta-expansions *)
    1.19         if_True, if_False, if_cancel, if_eq_cancel,
    1.20         imp_disjL, conj_assoc, disj_assoc,
    1.21         de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,