changeset 22822 | c1a6a2159e69 |
parent 22128 | cdd92316dd31 |
child 26288 | 89b9f7c18631 |
--- a/src/FOL/simpdata.ML Fri Apr 27 14:21:23 2007 +0200 +++ b/src/FOL/simpdata.ML Fri Apr 27 16:31:20 2007 +0200 @@ -275,11 +275,6 @@ (*** Standard simpsets ***) -structure Induction = InductionFun(struct val spec = spec end); - -open Induction; - - bind_thms ("meta_simps", [triv_forall_equality, (* prunes params *) thm "True_implies_equals"]); (* prune asms `True' *)