src/HOL/Tools/nat_arith.ML
changeset 35064 1bdef0c013d3
parent 35047 1b2bae06c796
child 35092 cfe605c54e50
     1.1 --- a/src/HOL/Tools/nat_arith.ML	Tue Feb 09 11:07:14 2010 +0100
     1.2 +++ b/src/HOL/Tools/nat_arith.ML	Tue Feb 09 11:47:47 2010 +0100
     1.3 @@ -51,7 +51,7 @@
     1.4    val dest_sum = dest_sum;
     1.5    val prove_conv = Arith_Data.prove_conv2;
     1.6    val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
     1.7 -    @{thm add_0}, @{thm Nat.add_0_right}];
     1.8 +    @{thm Nat.add_0}, @{thm Nat.add_0_right}];
     1.9    val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
    1.10    fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
    1.11    fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}