src/HOL/Nat.thy
changeset 48560 e0875d956a6b
parent 48559 686cc7c47589
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Nat.thy	Fri Jul 27 17:57:31 2012 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri Jul 27 17:59:18 2012 +0200
     1.3 @@ -11,7 +11,6 @@
     1.4  imports Inductive Typedef Fun Fields
     1.5  uses
     1.6    "~~/src/Tools/rat.ML"
     1.7 -  "~~/src/Provers/Arith/cancel_sums.ML"
     1.8    "Tools/arith_data.ML"
     1.9    ("Tools/nat_arith.ML")
    1.10    "~~/src/Provers/Arith/fast_lin_arith.ML"
    1.11 @@ -1497,19 +1496,19 @@
    1.12  
    1.13  simproc_setup nateq_cancel_sums
    1.14    ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
    1.15 -  {* fn phi => Nat_Arith.nateq_cancel_sums *}
    1.16 +  {* fn phi => fn ss => try Nat_Arith.cancel_eq_conv *}
    1.17  
    1.18  simproc_setup natless_cancel_sums
    1.19    ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
    1.20 -  {* fn phi => Nat_Arith.natless_cancel_sums *}
    1.21 +  {* fn phi => fn ss => try Nat_Arith.cancel_less_conv *}
    1.22  
    1.23  simproc_setup natle_cancel_sums
    1.24    ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") =
    1.25 -  {* fn phi => Nat_Arith.natle_cancel_sums *}
    1.26 +  {* fn phi => fn ss => try Nat_Arith.cancel_le_conv *}
    1.27  
    1.28  simproc_setup natdiff_cancel_sums
    1.29    ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
    1.30 -  {* fn phi => Nat_Arith.natdiff_cancel_sums *}
    1.31 +  {* fn phi => fn ss => try Nat_Arith.cancel_diff_conv *}
    1.32  
    1.33  use "Tools/lin_arith.ML"
    1.34  setup {* Lin_Arith.global_setup *}