--- a/src/HOL/Nat.thy Wed Jun 29 17:35:46 2011 +0200
+++ b/src/HOL/Nat.thy Wed Jun 29 18:12:34 2011 +0200
@@ -1433,6 +1433,15 @@
setup {* Lin_Arith.global_setup *}
declaration {* K Lin_Arith.setup *}
+simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) <= n" | "(m::nat) = n") =
+ {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
+(* Because of this simproc, the arithmetic solver is really only
+useful to detect inconsistencies among the premises for subgoals which are
+*not* themselves (in)equalities, because the latter activate
+fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
+solver all the time rather than add the additional check. *)
+
+
lemmas [arith_split] = nat_diff_split split_min split_max
context order