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.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.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