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