| changeset 45620 | f2a587696afb |
| parent 43597 | b4a093e755db |
| child 45622 | 4334c91b7405 |
--- a/src/HOL/Tools/simpdata.ML Wed Nov 23 22:07:55 2011 +0100 +++ b/src/HOL/Tools/simpdata.ML Wed Nov 23 22:59:39 2011 +0100 @@ -145,9 +145,6 @@ val split_tac = Splitter.split_tac; val split_inside_tac = Splitter.split_inside_tac; -val op addsplits = Splitter.addsplits; -val op delsplits = Splitter.delsplits; - (* integration of simplifier with classical reasoner *)