src/HOL/Tools/nat_arith.ML
changeset 35047 1b2bae06c796
parent 34974 18b41bba42b5
child 35064 1bdef0c013d3
     1.1 --- a/src/HOL/Tools/nat_arith.ML	Mon Feb 08 17:12:24 2010 +0100
     1.2 +++ b/src/HOL/Tools/nat_arith.ML	Mon Feb 08 17:12:27 2010 +0100
     1.3 @@ -50,8 +50,8 @@
     1.4    val mk_sum = mk_norm_sum;
     1.5    val dest_sum = dest_sum;
     1.6    val prove_conv = Arith_Data.prove_conv2;
     1.7 -  val norm_tac1 = Arith_Data.simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
     1.8 -    @{thm "add_0"}, @{thm "add_0_right"}];
     1.9 +  val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
    1.10 +    @{thm add_0}, @{thm Nat.add_0_right}];
    1.11    val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
    1.12    fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
    1.13    fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}