equal
deleted
inserted
replaced
60 fun unsafe_solver ctxt = |
60 fun unsafe_solver ctxt = |
61 FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), assume_tac]; |
61 FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), assume_tac]; |
62 |
62 |
63 (*No premature instantiation of variables during simplification*) |
63 (*No premature instantiation of variables during simplification*) |
64 fun safe_solver ctxt = |
64 fun safe_solver ctxt = |
65 FIRST' [fn i => DETERM (match_tac (triv_rls @ Simplifier.prems_of ctxt) i), eq_assume_tac]; |
65 FIRST' [fn i => DETERM (match_tac ctxt (triv_rls @ Simplifier.prems_of ctxt) i), |
|
66 eq_assume_tac]; |
66 |
67 |
67 (*No simprules, but basic infrastructure for simplification*) |
68 (*No simprules, but basic infrastructure for simplification*) |
68 val LK_basic_ss = |
69 val LK_basic_ss = |
69 empty_simpset @{context} |
70 empty_simpset @{context} |
70 setSSolver (mk_solver "safe" safe_solver) |
71 setSSolver (mk_solver "safe" safe_solver) |