164 [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]), |
164 [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]), |
165 ("All", [@{thm spec}]), ("True", []), ("False", []), |
165 ("All", [@{thm spec}]), ("True", []), ("False", []), |
166 ("HOL.If", [@{thm if_bool_eq_conj} RS @{thm iffD1}])]; |
166 ("HOL.If", [@{thm if_bool_eq_conj} RS @{thm iffD1}])]; |
167 |
167 |
168 val HOL_basic_ss = |
168 val HOL_basic_ss = |
169 Simplifier.theory_context (the_context ()) empty_ss |
169 Simplifier.theory_context @{theory} empty_ss |
170 setsubgoaler asm_simp_tac |
170 setsubgoaler asm_simp_tac |
171 setSSolver safe_solver |
171 setSSolver safe_solver |
172 setSolver unsafe_solver |
172 setSolver unsafe_solver |
173 setmksimps (mksimps mksimps_pairs) |
173 setmksimps (mksimps mksimps_pairs) |
174 setmkeqTrue mk_eq_True |
174 setmkeqTrue mk_eq_True |