src/HOL/Nat.thy
changeset 61144 5e94dfead1c2
parent 61076 bdc1e2f0a86a
child 61169 4de9ff3ea29a
     1.1 --- a/src/HOL/Nat.thy	Wed Sep 09 14:47:41 2015 +0200
     1.2 +++ b/src/HOL/Nat.thy	Wed Sep 09 20:57:21 2015 +0200
     1.3 @@ -1664,8 +1664,8 @@
     1.4  setup \<open>Lin_Arith.global_setup\<close>
     1.5  declaration \<open>K Lin_Arith.setup\<close>
     1.6  
     1.7 -simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) <= n" | "(m::nat) = n") =
     1.8 -  \<open>fn _ => fn ss => fn ct => Lin_Arith.simproc ss (Thm.term_of ct)\<close>
     1.9 +simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \<le> n" | "(m::nat) = n") =
    1.10 +  \<open>K Lin_Arith.simproc\<close>
    1.11  (* Because of this simproc, the arithmetic solver is really only
    1.12  useful to detect inconsistencies among the premises for subgoals which are
    1.13  *not* themselves (in)equalities, because the latter activate