390 eta_contract_eq, (* prunes eta-expansions *) |
390 eta_contract_eq, (* prunes eta-expansions *) |
391 if_True, if_False, if_cancel, if_eq_cancel, |
391 if_True, if_False, if_cancel, if_eq_cancel, |
392 imp_disjL, conj_assoc, disj_assoc, |
392 imp_disjL, conj_assoc, disj_assoc, |
393 de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp, |
393 de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp, |
394 disj_not1, not_all, not_ex, cases_simp, some_eq_trivial, some_sym_eq_trivial, |
394 disj_not1, not_all, not_ex, cases_simp, some_eq_trivial, some_sym_eq_trivial, |
395 thm"plus_ac0.zero", thm"plus_ac0_zero_right"] |
395 thm "the_eq_trivial", the_sym_eq_trivial, thm "plus_ac0.zero", thm "plus_ac0_zero_right"] |
396 @ ex_simps @ all_simps @ simp_thms) |
396 @ ex_simps @ all_simps @ simp_thms) |
397 addsimprocs [defALL_regroup,defEX_regroup] |
397 addsimprocs [defALL_regroup,defEX_regroup] |
398 addcongs [imp_cong] |
398 addcongs [imp_cong] |
399 addsplits [split_if]; |
399 addsplits [split_if]; |
400 |
400 |