src/HOL/Library/Extended_Nat.thy
changeset 57514 bdc2c6b40bf2
parent 57512 cc97b347b301
child 58306 117ba6cbe414
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -169,10 +169,10 @@
     1.4  lemma plus_1_eSuc:
     1.5    "1 + q = eSuc q"
     1.6    "q + 1 = eSuc q"
     1.7 -  by (simp_all add: eSuc_plus_1 add_ac)
     1.8 +  by (simp_all add: eSuc_plus_1 ac_simps)
     1.9  
    1.10  lemma iadd_Suc: "eSuc m + n = eSuc (m + n)"
    1.11 -  by (simp_all add: eSuc_plus_1 add_ac)
    1.12 +  by (simp_all add: eSuc_plus_1 ac_simps)
    1.13  
    1.14  lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)"
    1.15    by (simp only: add.commute[of m] iadd_Suc)
    1.16 @@ -523,7 +523,7 @@
    1.17    val trans_tac = Numeral_Simprocs.trans_tac
    1.18    val norm_ss =
    1.19      simpset_of (put_simpset HOL_basic_ss @{context}
    1.20 -      addsimps @{thms add_ac add_0_left add_0_right})
    1.21 +      addsimps @{thms ac_simps add_0_left add_0_right})
    1.22    fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
    1.23    fun simplify_meta_eq ctxt cancel_th th =
    1.24      Arith_Data.simplify_meta_eq [] ctxt