src/HOL/Tools/nat_arith.ML
changeset 38715 6513ea67d95d
parent 35267 8dfd816713c6
child 38864 4abe644fcea5
     1.1 --- a/src/HOL/Tools/nat_arith.ML	Wed Aug 25 18:19:04 2010 +0200
     1.2 +++ b/src/HOL/Tools/nat_arith.ML	Wed Aug 25 18:36:22 2010 +0200
     1.3 @@ -91,18 +91,18 @@
     1.4  end);
     1.5  
     1.6  val nat_cancel_sums_add =
     1.7 -  [Simplifier.simproc @{theory} "nateq_cancel_sums"
     1.8 +  [Simplifier.simproc_global @{theory} "nateq_cancel_sums"
     1.9       ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
    1.10       (K EqCancelSums.proc),
    1.11 -   Simplifier.simproc @{theory} "natless_cancel_sums"
    1.12 +   Simplifier.simproc_global @{theory} "natless_cancel_sums"
    1.13       ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
    1.14       (K LessCancelSums.proc),
    1.15 -   Simplifier.simproc @{theory} "natle_cancel_sums"
    1.16 +   Simplifier.simproc_global @{theory} "natle_cancel_sums"
    1.17       ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
    1.18       (K LeCancelSums.proc)];
    1.19  
    1.20  val nat_cancel_sums = nat_cancel_sums_add @
    1.21 -  [Simplifier.simproc @{theory} "natdiff_cancel_sums"
    1.22 +  [Simplifier.simproc_global @{theory} "natdiff_cancel_sums"
    1.23      ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
    1.24      (K DiffCancelSums.proc)];
    1.25