| changeset 82697 | cc05bc2cfb2f |
| parent 82696 | 032c2aac4454 |
| child 82698 | c0f166b39a3a |
| 82696:032c2aac4454 | 82697:cc05bc2cfb2f |
|---|---|
1 (* Title: Tools/simp_legacy.ML |
|
2 |
|
3 Legacy simplifier configuration interfaces -- to be phased out eventually. |
|
4 *) |
|
5 |
|
6 infix 4 addsimps delsimps addsimprocs delsimprocs; |
|
7 |
|
8 fun ctxt addsimps thms = ctxt |> Simplifier.add_simps thms; |
|
9 fun ctxt delsimps thms = ctxt |> Simplifier.del_simps thms; |
|
10 |
|
11 fun ctxt addsimprocs procs = ctxt |> fold Simplifier.add_proc procs; |
|
12 fun ctxt delsimprocs procs = ctxt |> fold Simplifier.del_proc procs; |