362 |
362 |
363 val HOL_ss = |
363 val HOL_ss = |
364 HOL_basic_ss addsimps |
364 HOL_basic_ss addsimps |
365 ([triv_forall_equality, (* prunes params *) |
365 ([triv_forall_equality, (* prunes params *) |
366 True_implies_equals, (* prune asms `True' *) |
366 True_implies_equals, (* prune asms `True' *) |
367 eta_contract_eq, (* prunes eta-expansions *) |
|
368 if_True, if_False, if_cancel, if_eq_cancel, |
367 if_True, if_False, if_cancel, if_eq_cancel, |
369 imp_disjL, conj_assoc, disj_assoc, |
368 imp_disjL, conj_assoc, disj_assoc, |
370 de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp, |
369 de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp, |
371 disj_not1, not_all, not_ex, cases_simp, |
370 disj_not1, not_all, not_ex, cases_simp, |
372 thm "the_eq_trivial", the_sym_eq_trivial] |
371 thm "the_eq_trivial", the_sym_eq_trivial] |