equal
deleted
inserted
replaced
19 |
19 |
20 begin |
20 begin |
21 |
21 |
22 defaultsort pcpo |
22 defaultsort pcpo |
23 |
23 |
24 ML_setup {* |
24 declaration {* fn _ => |
25 change_simpset (fn simpset => simpset addSolver |
25 Simplifier.map_ss (fn simpset => simpset addSolver |
26 (mk_solver' "adm_tac" (fn ss => |
26 (mk_solver' "adm_tac" (fn ss => |
27 adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss)))); |
27 adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss)))); |
28 *} |
28 *} |
29 |
29 |
30 end |
30 end |