| changeset 54388 | 8b165615ffe3 |
| parent 51930 | 52fd62618631 |
| child 58838 | 59203adfc33f |
| 54387:890e983cb07b | 54388:8b165615ffe3 |
|---|---|
105 |
105 |
106 |
106 |
107 val conv = Simplifier.simproc_global @{theory} "data_free" ["(x::i) = y"] proc; |
107 val conv = Simplifier.simproc_global @{theory} "data_free" ["(x::i) = y"] proc; |
108 |
108 |
109 end; |
109 end; |
110 *} |
|
110 |
111 |
111 |
112 setup {* |
112 Addsimprocs [DataFree.conv]; |
113 Simplifier.map_theory_simpset (fn ctxt => ctxt addsimprocs [DataFree.conv]) |
113 *} |
114 *} |
114 |
115 |
115 end |
116 end |