src/HOL/Int.thy
changeset 61144 5e94dfead1c2
parent 61076 bdc1e2f0a86a
child 61169 4de9ff3ea29a
     1.1 --- a/src/HOL/Int.thy	Wed Sep 09 14:47:41 2015 +0200
     1.2 +++ b/src/HOL/Int.thy	Wed Sep 09 20:57:21 2015 +0200
     1.3 @@ -775,9 +775,9 @@
     1.4  declaration \<open>K Int_Arith.setup\<close>
     1.5  
     1.6  simproc_setup fast_arith ("(m::'a::linordered_idom) < n" |
     1.7 -  "(m::'a::linordered_idom) <= n" |
     1.8 +  "(m::'a::linordered_idom) \<le> n" |
     1.9    "(m::'a::linordered_idom) = n") =
    1.10 -  \<open>fn _ => fn ss => fn ct => Lin_Arith.simproc ss (Thm.term_of ct)\<close>
    1.11 +  \<open>K Lin_Arith.simproc\<close>
    1.12  
    1.13  
    1.14  subsection\<open>More Inequality Reasoning\<close>