equal
deleted
inserted
replaced
323 eq_assume_tac, ematch_tac [FalseE]]; |
323 eq_assume_tac, ematch_tac [FalseE]]; |
324 |
324 |
325 (*No simprules, but basic infastructure for simplification*) |
325 (*No simprules, but basic infastructure for simplification*) |
326 val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac |
326 val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac |
327 addsimprocs [defALL_regroup,defEX_regroup] |
327 addsimprocs [defALL_regroup,defEX_regroup] |
328 setSSolver safe_solver |
328 setSSolver (mk_solver "FOL safe" safe_solver) |
329 setSolver unsafe_solver |
329 setSolver (mk_solver "FOL unsafe" unsafe_solver) |
330 setmksimps (mksimps mksimps_pairs); |
330 setmksimps (mksimps mksimps_pairs); |
331 |
331 |
332 |
332 |
333 |
333 |
334 (*intuitionistic simprules only*) |
334 (*intuitionistic simprules only*) |