equal
deleted
inserted
replaced
1 (* Title: Tools/simp_legacy.ML |
1 (* Title: Tools/simp_legacy.ML |
2 |
2 |
3 Legacy simplifier configuration interfaces -- to be phased out eventually. |
3 Legacy simplifier configuration interfaces -- to be phased out eventually. |
4 *) |
4 *) |
5 |
5 |
6 infix 4 |
6 infix 4 addsimps delsimps addsimprocs delsimprocs; |
7 addsimps delsimps addsimprocs delsimprocs |
|
8 setloop addloop delloop |
|
9 setSSolver addSSolver setSolver addSolver; |
|
10 |
7 |
11 local |
8 fun ctxt addsimps thms = ctxt |> Simplifier.add_simps thms; |
|
9 fun ctxt delsimps thms = ctxt |> Simplifier.del_simps thms; |
12 |
10 |
13 open Simplifier |
11 fun ctxt addsimprocs procs = ctxt |> fold Simplifier.add_proc procs; |
14 |
12 fun ctxt delsimprocs procs = ctxt |> fold Simplifier.del_proc procs; |
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 |
|