src/ZF/arith_data.ML

 		    "succ(m) #- n", "m #- succ(n)"],
 	 DiffCancelNumerals.proc)];
 
 end;
 
+(*Install the simprocs!*)
+Addsimprocs ArithData.nat_cancel;
+
+
 (*examples:
 print_depth 22;
 set timing;
 set trace_simp;
 fun test s = (Goal s; by (Asm_simp_tac 1));