equal
deleted
inserted
replaced
92 infix addcongs; |
92 infix addcongs; |
93 fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]); |
93 fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]); |
94 |
94 |
95 val HOL_ss = empty_ss |
95 val HOL_ss = empty_ss |
96 setmksimps mk_rews |
96 setmksimps mk_rews |
97 setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac) |
97 setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac |
|
98 ORELSE' etac FalseE) |
98 setsubgoaler asm_simp_tac |
99 setsubgoaler asm_simp_tac |
99 addsimps ([if_True, if_False, o_apply, conj_assoc] @ simp_thms) |
100 addsimps ([if_True, if_False, o_apply, conj_assoc] @ simp_thms) |
100 addcongs [imp_cong]; |
101 addcongs [imp_cong]; |
101 |
102 |
102 fun split_tac splits = |
103 fun split_tac splits = |