equal
deleted
inserted
replaced
239 fun safe_solver prems = FIRST'[fn i => DETERM (match_tac (triv_rls@prems) i), |
239 fun safe_solver prems = FIRST'[fn i => DETERM (match_tac (triv_rls@prems) i), |
240 eq_assume_tac]; |
240 eq_assume_tac]; |
241 |
241 |
242 (*No simprules, but basic infrastructure for simplification*) |
242 (*No simprules, but basic infrastructure for simplification*) |
243 val LK_basic_ss = empty_ss setsubgoaler asm_simp_tac |
243 val LK_basic_ss = empty_ss setsubgoaler asm_simp_tac |
244 setSSolver safe_solver |
244 setSSolver (mk_solver "safe" safe_solver) |
245 setSolver unsafe_solver |
245 setSolver (mk_solver "unsafe" unsafe_solver) |
246 setmksimps (map mk_meta_eq o atomize o gen_all); |
246 setmksimps (map mk_meta_eq o atomize o gen_all); |
247 |
247 |
248 val LK_simps = |
248 val LK_simps = |
249 [triv_forall_equality, (* prunes params *) |
249 [triv_forall_equality, (* prunes params *) |
250 refl RS P_iff_T] @ |
250 refl RS P_iff_T] @ |