# HG changeset patch
# User nipkow
# Date 1025520635 -7200
# Node ID a0460a450cf9e5c7bf2da3c591ef29b93104aee0
# Parent  ea36a40c004fc18bfd6c054bf3b247478e621b2b
fixed problem with linear arith.

diff -r ea36a40c004f -r a0460a450cf9 src/HOL/Integ/nat_bin.ML
--- a/src/HOL/Integ/nat_bin.ML	Sat Jun 29 22:46:56 2002 +0200
+++ b/src/HOL/Integ/nat_bin.ML	Mon Jul 01 12:50:35 2002 +0200
@@ -44,15 +44,6 @@
 Addsimps [int_nat_number_of];
 
 
-val nat_bin_arith_setup =
- [Fast_Arith.map_data 
-   (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
-     {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
-      inj_thms = inj_thms,
-      lessD = lessD,
-      simpset = simpset addsimps [int_nat_number_of, not_neg_number_of_Pls,
-                                  neg_number_of_Min,neg_number_of_BIT]})];
-
 (** Successor **)
 
 Goal "(0::int) <= z ==> Suc (nat z) = nat (1 + z)";
@@ -75,6 +66,16 @@
 qed "Suc_nat_number_of";
 Addsimps [Suc_nat_number_of];
 
+val nat_bin_arith_setup =
+ [Fast_Arith.map_data 
+   (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
+     {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
+      inj_thms = inj_thms,
+      lessD = lessD,
+      simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
+                                  not_neg_number_of_Pls,
+                                  neg_number_of_Min,neg_number_of_BIT]})];
+
 (** Addition **)
 
 Goal "[| (0::int) <= z;  0 <= z' |] ==> nat (z+z') = nat z + nat z'";