src/HOL/Integ/NatSimprocs.ML

 Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
 
 
 (*examples:
 print_depth 22;
-set proof_timing;
+set timing;
 set trace_simp;
 fun test s = (Goal s; by (Simp_tac 1)); 
 
 (*cancel_numerals*)
 test "l +( #2) + (#2) + #2 + (l + #2) + (oo  + #2) = (uu::nat)";