--- a/src/HOL/ex/NatSum.ML Mon Jan 12 17:26:00 1998 +0100
+++ b/src/HOL/ex/NatSum.ML Mon Jan 12 17:26:34 1998 +0100
@@ -7,6 +7,7 @@
Demonstrates permutative rewriting.
*)
+Delsimprocs nat_cancel;
Addsimps add_ac;
Addsimps [add_mult_distrib, add_mult_distrib2];