src/HOL/Nat.thy
changeset 54742 7a86358a3c0b
parent 54496 178922b63b58
child 55415 05f5fdb8d093
     1.1 --- a/src/HOL/Nat.thy	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/Nat.thy	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -1536,19 +1536,19 @@
     1.4  
     1.5  simproc_setup nateq_cancel_sums
     1.6    ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
     1.7 -  {* fn phi => fn ss => try Nat_Arith.cancel_eq_conv *}
     1.8 +  {* fn phi => try o Nat_Arith.cancel_eq_conv *}
     1.9  
    1.10  simproc_setup natless_cancel_sums
    1.11    ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
    1.12 -  {* fn phi => fn ss => try Nat_Arith.cancel_less_conv *}
    1.13 +  {* fn phi => try o Nat_Arith.cancel_less_conv *}
    1.14  
    1.15  simproc_setup natle_cancel_sums
    1.16    ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") =
    1.17 -  {* fn phi => fn ss => try Nat_Arith.cancel_le_conv *}
    1.18 +  {* fn phi => try o Nat_Arith.cancel_le_conv *}
    1.19  
    1.20  simproc_setup natdiff_cancel_sums
    1.21    ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
    1.22 -  {* fn phi => fn ss => try Nat_Arith.cancel_diff_conv *}
    1.23 +  {* fn phi => try o Nat_Arith.cancel_diff_conv *}
    1.24  
    1.25  ML_file "Tools/lin_arith.ML"
    1.26  setup {* Lin_Arith.global_setup *}