equal
deleted
inserted
replaced
296 val HOL_ss = empty_ss |
296 val HOL_ss = empty_ss |
297 setmksimps (mksimps mksimps_pairs) |
297 setmksimps (mksimps mksimps_pairs) |
298 setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac |
298 setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac |
299 ORELSE' etac FalseE) |
299 ORELSE' etac FalseE) |
300 setsubgoaler asm_simp_tac |
300 setsubgoaler asm_simp_tac |
301 addsimps ([if_True, if_False, if_cancel, |
301 addsimps ([if_True, if_False, o_apply, imp_disjL, conj_assoc, disj_assoc, |
302 o_apply, imp_disjL, conj_assoc, disj_assoc, |
|
303 de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp] |
302 de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp] |
304 @ ex_simps @ all_simps @ simp_thms) |
303 @ ex_simps @ all_simps @ simp_thms) |
305 addcongs [imp_cong]; |
304 addcongs [imp_cong]; |
306 |
305 |
307 |
306 |
329 |
328 |
330 |
329 |
331 |
330 |
332 (*** Install simpsets and datatypes in theory structure ***) |
331 (*** Install simpsets and datatypes in theory structure ***) |
333 |
332 |
334 simpset := HOL_ss; |
333 simpset := HOL_ss addsimps [if_cancel]; |
335 |
334 |
336 exception SS_DATA of simpset; |
335 exception SS_DATA of simpset; |
337 |
336 |
338 let fun merge [] = SS_DATA empty_ss |
337 let fun merge [] = SS_DATA empty_ss |
339 | merge ss = let val ss = map (fn SS_DATA x => x) ss; |
338 | merge ss = let val ss = map (fn SS_DATA x => x) ss; |