src/HOL/Nat.thy
changeset 48559 686cc7c47589
parent 47988 e4b69e10b990
child 48560 e0875d956a6b
     1.1 --- a/src/HOL/Nat.thy	Fri Jul 27 17:34:33 2012 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri Jul 27 17:57:31 2012 +0200
     1.3 @@ -1494,7 +1494,22 @@
     1.4  setup Arith_Data.setup
     1.5  
     1.6  use "Tools/nat_arith.ML"
     1.7 -declaration {* K Nat_Arith.setup *}
     1.8 +
     1.9 +simproc_setup nateq_cancel_sums
    1.10 +  ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
    1.11 +  {* fn phi => Nat_Arith.nateq_cancel_sums *}
    1.12 +
    1.13 +simproc_setup natless_cancel_sums
    1.14 +  ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
    1.15 +  {* fn phi => Nat_Arith.natless_cancel_sums *}
    1.16 +
    1.17 +simproc_setup natle_cancel_sums
    1.18 +  ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") =
    1.19 +  {* fn phi => Nat_Arith.natle_cancel_sums *}
    1.20 +
    1.21 +simproc_setup natdiff_cancel_sums
    1.22 +  ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
    1.23 +  {* fn phi => Nat_Arith.natdiff_cancel_sums *}
    1.24  
    1.25  use "Tools/lin_arith.ML"
    1.26  setup {* Lin_Arith.global_setup *}