deleted redundant (looping!) simprule
authorpaulson
Wed Dec 14 18:01:50 2005 +0100 (2005-12-14)
changeset 18407fa075b606571
parent 18406 b1eab0eb7fec
child 18408 07da804d1119
deleted redundant (looping!) simprule
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Wed Dec 14 16:14:41 2005 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Wed Dec 14 18:01:50 2005 +0100
     1.3 @@ -364,7 +364,6 @@
     1.4      HOL_basic_ss addsimps
     1.5       ([triv_forall_equality, (* prunes params *)
     1.6         True_implies_equals, (* prune asms `True' *)
     1.7 -       eta_contract_eq, (* prunes eta-expansions *)
     1.8         if_True, if_False, if_cancel, if_eq_cancel,
     1.9         imp_disjL, conj_assoc, disj_assoc,
    1.10         de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,