equal
deleted
inserted
replaced
143 ); |
143 ); |
144 |
144 |
145 val split_tac = Splitter.split_tac; |
145 val split_tac = Splitter.split_tac; |
146 val split_inside_tac = Splitter.split_inside_tac; |
146 val split_inside_tac = Splitter.split_inside_tac; |
147 |
147 |
148 val op addsplits = Splitter.addsplits; |
|
149 val op delsplits = Splitter.delsplits; |
|
150 |
|
151 |
148 |
152 (* integration of simplifier with classical reasoner *) |
149 (* integration of simplifier with classical reasoner *) |
153 |
150 |
154 structure Clasimp = Clasimp |
151 structure Clasimp = Clasimp |
155 ( |
152 ( |