| changeset 38715 | 6513ea67d95d |
| parent 38522 | de7984a7172b |
| child 41777 | 1f7cbe39d425 |
| 38714:31da698fc4e5 | 38715:6513ea67d95d |
|---|---|
99 raise Match) |
99 raise Match) |
100 in SOME thm end |
100 in SOME thm end |
101 handle Match => NONE; |
101 handle Match => NONE; |
102 |
102 |
103 |
103 |
104 val conv = Simplifier.simproc @{theory} "data_free" ["(x::i) = y"] proc; |
104 val conv = Simplifier.simproc_global @{theory} "data_free" ["(x::i) = y"] proc; |
105 |
105 |
106 end; |
106 end; |
107 |
107 |
108 |
108 |
109 Addsimprocs [DataFree.conv]; |
109 Addsimprocs [DataFree.conv]; |