|
82663
|
1 |
(* Title: Tools/simp_legacy.ML
|
|
|
2 |
|
|
|
3 |
Legacy simplifier configuration interfaces -- to be phased out eventually.
|
|
|
4 |
*)
|
|
|
5 |
|
|
|
6 |
infix 4
|
|
|
7 |
addsimps delsimps addsimprocs delsimprocs
|
|
|
8 |
setloop addloop delloop
|
|
|
9 |
setSSolver addSSolver setSolver addSolver;
|
|
|
10 |
|
|
|
11 |
local
|
|
|
12 |
|
|
|
13 |
open Simplifier
|
|
|
14 |
|
|
|
15 |
in
|
|
|
16 |
|
|
|
17 |
fun ctxt addsimps thms = ctxt |> add_simps thms;
|
|
|
18 |
fun ctxt delsimps thms = ctxt |> del_simps thms;
|
|
|
19 |
|
|
|
20 |
fun ctxt addsimprocs procs = ctxt |> fold add_proc procs;
|
|
|
21 |
fun ctxt delsimprocs procs = ctxt |> fold del_proc procs;
|
|
|
22 |
|
|
|
23 |
fun ctxt setloop looper = ctxt |> set_loop looper;
|
|
|
24 |
fun ctxt addloop looper = ctxt |> add_loop looper;
|
|
|
25 |
fun ctxt delloop looper = ctxt |> del_loop looper;
|
|
|
26 |
|
|
|
27 |
fun ctxt setSSolver solver = ctxt |> set_safe_solver solver;
|
|
|
28 |
fun ctxt addSSolver solver = ctxt |> add_safe_solver solver;
|
|
|
29 |
|
|
|
30 |
fun ctxt setSolver solver = ctxt |> set_unsafe_solver solver;
|
|
|
31 |
fun ctxt addSolver solver = ctxt |> add_unsafe_solver solver;
|
|
|
32 |
|
|
|
33 |
end
|