src/HOL/Library/Extended_Nat.thy
changeset 51717 9e7d1c139569
parent 51366 abdcf1a7cabf
child 52729 412c9e0381a1
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -507,11 +507,12 @@
     1.4    fun dest_sum t = dest_summing (t, [])
     1.5    val find_first = find_first_t []
     1.6    val trans_tac = Numeral_Simprocs.trans_tac
     1.7 -  val norm_ss = HOL_basic_ss addsimps
     1.8 -    @{thms add_ac add_0_left add_0_right}
     1.9 -  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
    1.10 -  fun simplify_meta_eq ss cancel_th th =
    1.11 -    Arith_Data.simplify_meta_eq [] ss
    1.12 +  val norm_ss =
    1.13 +    simpset_of (put_simpset HOL_basic_ss @{context}
    1.14 +      addsimps @{thms add_ac add_0_left add_0_right})
    1.15 +  fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
    1.16 +  fun simplify_meta_eq ctxt cancel_th th =
    1.17 +    Arith_Data.simplify_meta_eq [] ctxt
    1.18        ([th, cancel_th] MRS trans)
    1.19    fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
    1.20  end
    1.21 @@ -540,15 +541,15 @@
    1.22  
    1.23  simproc_setup enat_eq_cancel
    1.24    ("(l::enat) + m = n" | "(l::enat) = m + n") =
    1.25 -  {* fn phi => fn ss => fn ct => Eq_Enat_Cancel.proc ss (term_of ct) *}
    1.26 +  {* fn phi => fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (term_of ct) *}
    1.27  
    1.28  simproc_setup enat_le_cancel
    1.29    ("(l::enat) + m \<le> n" | "(l::enat) \<le> m + n") =
    1.30 -  {* fn phi => fn ss => fn ct => Le_Enat_Cancel.proc ss (term_of ct) *}
    1.31 +  {* fn phi => fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (term_of ct) *}
    1.32  
    1.33  simproc_setup enat_less_cancel
    1.34    ("(l::enat) + m < n" | "(l::enat) < m + n") =
    1.35 -  {* fn phi => fn ss => fn ct => Less_Enat_Cancel.proc ss (term_of ct) *}
    1.36 +  {* fn phi => fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (term_of ct) *}
    1.37  
    1.38  text {* TODO: add regression tests for these simprocs *}
    1.39