author | paulson |
Wed, 14 Dec 2005 18:01:50 +0100 | |
changeset 18407 | fa075b606571 |
parent 18406 | b1eab0eb7fec |
child 18408 | 07da804d1119 |
--- a/src/HOL/simpdata.ML Wed Dec 14 16:14:41 2005 +0100 +++ b/src/HOL/simpdata.ML Wed Dec 14 18:01:50 2005 +0100 @@ -364,7 +364,6 @@ HOL_basic_ss addsimps ([triv_forall_equality, (* prunes params *) True_implies_equals, (* prune asms `True' *) - eta_contract_eq, (* prunes eta-expansions *) if_True, if_False, if_cancel, if_eq_cancel, imp_disjL, conj_assoc, disj_assoc, de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,