src/HOL/Tools/nat_numeral_simprocs.ML
changeset 31790 05c92381363c
parent 31368 763f4b0fd579
child 32010 cb1a1c94b4cd
     1.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Tue Jun 23 21:07:39 2009 +0200
     1.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Wed Jun 24 09:41:14 2009 +0200
     1.3 @@ -152,7 +152,7 @@
     1.4    fun trans_tac _       = Arith_Data.trans_tac
     1.5  
     1.6    val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
     1.7 -    [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
     1.8 +    [@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
     1.9    val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
    1.10    fun norm_tac ss = 
    1.11      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    1.12 @@ -240,7 +240,7 @@
    1.13    val prove_conv        = Arith_Data.prove_conv_nohyps
    1.14    fun trans_tac _       = Arith_Data.trans_tac
    1.15  
    1.16 -  val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
    1.17 +  val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms add_ac}
    1.18    val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
    1.19    fun norm_tac ss =
    1.20      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    1.21 @@ -266,7 +266,7 @@
    1.22    fun trans_tac _       = Arith_Data.trans_tac
    1.23  
    1.24    val norm_ss1 = Numeral_Simprocs.num_ss addsimps
    1.25 -    numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
    1.26 +    numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
    1.27    val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
    1.28    fun norm_tac ss =
    1.29      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))