# HG changeset patch
# User haftmann
# Date 1157543282 -7200
# Node ID 3078fd2eec7bd3d7d6b8d1786947c37ed5ddfbbe
# Parent  3d3d24186352d5d637f776b46d4bcc5123ef9508
got rid of Numeral.bin type

diff -r 3d3d24186352 -r 3078fd2eec7b NEWS
--- a/NEWS	Wed Sep 06 10:01:27 2006 +0200
+++ b/NEWS	Wed Sep 06 13:48:02 2006 +0200
@@ -465,6 +465,20 @@
 
 *** HOL ***
 
+* Numeral syntax: type 'bin' which was a mere type copy of 'int' has been
+abandoned in favour of plain 'int'. Significant changes for setting up numeral
+syntax for types:
+
+  - new constants Numeral.pred and Numeral.succ instead
+      of former Numeral.bin_pred and Numeral.bin_succ.
+  - Use integer operations instead of bin_add, bin_mult and so on.
+  - Numeral simplification theorems named Numeral.numeral_simps instead of Bin_simps.
+  - ML structure Bin_Simprocs now named Int_Numeral_Base_Simprocs.
+
+See HOL/Integ/IntArith.thy for an example setup.
+
+INCOMPATIBILITY.
+
 * New top level command 'normal_form' computes the normal form of a term
 that may contain free variables. For example 'normal_form "rev[a,b,c]"'
 prints '[b,c,a]'. This command is suitable for heavy-duty computations
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Complex/Complex.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -830,7 +830,7 @@
 instance complex :: number ..
 
 defs (overloaded)
-  complex_number_of_def: "(number_of w :: complex) == of_int (Rep_Bin w)"
+  complex_number_of_def: "(number_of w :: complex) == of_int w"
     --{*the type constraint is essential!*}
 
 instance complex :: number_ring
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -783,7 +783,7 @@
 
 subsection{*Numerals and Arithmetic*}
 
-lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int (Rep_Bin w)"
+lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int w"
 by (transfer, rule number_of_eq [THEN eq_reflection])
 
 lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: 
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -547,7 +547,7 @@
 
 in
 val approx_reorient_simproc =
-  Bin_Simprocs.prep_simproc
+  Int_Numeral_Base_Simprocs.prep_simproc
     ("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc);
 end;
 
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Import/HOL/HOL4Prob.thy
--- a/src/HOL/Import/HOL/HOL4Prob.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Import/HOL/HOL4Prob.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -35,28 +35,28 @@
 lemma DIV_TWO_BASIC: "(op &::bool => bool => bool)
  ((op =::nat => nat => bool)
    ((op div::nat => nat => nat) (0::nat)
-     ((number_of::bin => nat)
-       ((op BIT::bin => bit => bin)
-         ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+     ((number_of \<Colon> int => nat)
+       ((op BIT \<Colon> int => bit => int)
+         ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
          (bit.B0::bit))))
    (0::nat))
  ((op &::bool => bool => bool)
    ((op =::nat => nat => bool)
      ((op div::nat => nat => nat) (1::nat)
-       ((number_of::bin => nat)
-         ((op BIT::bin => bit => bin)
-           ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+       ((number_of \<Colon> int => nat)
+         ((op BIT \<Colon> int => bit => int)
+           ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
            (bit.B0::bit))))
      (0::nat))
    ((op =::nat => nat => bool)
      ((op div::nat => nat => nat)
-       ((number_of::bin => nat)
-         ((op BIT::bin => bit => bin)
-           ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+       ((number_of \<Colon> int => nat)
+         ((op BIT \<Colon> int => bit => int)
+           ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
            (bit.B0::bit)))
-       ((number_of::bin => nat)
-         ((op BIT::bin => bit => bin)
-           ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+       ((number_of \<Colon> int => nat)
+         ((op BIT \<Colon> int => bit => int)
+           ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
            (bit.B0::bit))))
      (1::nat)))"
   by (import prob_extra DIV_TWO_BASIC)
@@ -75,19 +75,19 @@
      (op =::nat => nat => bool)
       ((op div::nat => nat => nat)
         ((op ^::nat => nat => nat)
-          ((number_of::bin => nat)
-            ((op BIT::bin => bit => bin)
-              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+          ((number_of \<Colon> int => nat)
+            ((op BIT \<Colon> int => bit => int)
+              ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
               (bit.B0::bit)))
           ((Suc::nat => nat) n))
-        ((number_of::bin => nat)
-          ((op BIT::bin => bit => bin)
-            ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+        ((number_of \<Colon> int => nat)
+          ((op BIT \<Colon> int => bit => int)
+            ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
             (bit.B0::bit))))
       ((op ^::nat => nat => nat)
-        ((number_of::bin => nat)
-          ((op BIT::bin => bit => bin)
-            ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+        ((number_of \<Colon> int => nat)
+          ((op BIT \<Colon> int => bit => int)
+            ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
             (bit.B0::bit)))
         n))"
   by (import prob_extra EXP_DIV_TWO)
@@ -125,22 +125,22 @@
 
 lemma HALF_POS: "(op <::real => real => bool) (0::real)
  ((op /::real => real => real) (1::real)
-   ((number_of::bin => real)
-     ((op BIT::bin => bit => bin)
-       ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+   ((number_of \<Colon> int => real)
+     ((op BIT \<Colon> int => bit => int)
+       ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
        (bit.B0::bit))))"
   by (import prob_extra HALF_POS)
 
 lemma HALF_CANCEL: "(op =::real => real => bool)
  ((op *::real => real => real)
-   ((number_of::bin => real)
-     ((op BIT::bin => bit => bin)
-       ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+   ((number_of \<Colon> int => real)
+     ((op BIT \<Colon> int => bit => int)
+       ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
        (bit.B0::bit)))
    ((op /::real => real => real) (1::real)
-     ((number_of::bin => real)
-       ((op BIT::bin => bit => bin)
-         ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+     ((number_of \<Colon> int => real)
+       ((op BIT \<Colon> int => bit => int)
+         ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
          (bit.B0::bit)))))
  (1::real)"
   by (import prob_extra HALF_CANCEL)
@@ -150,9 +150,9 @@
      (op <::real => real => bool) (0::real)
       ((op ^::real => nat => real)
         ((op /::real => real => real) (1::real)
-          ((number_of::bin => real)
-            ((op BIT::bin => bit => bin)
-              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+          ((number_of \<Colon> int => real)
+            ((op BIT \<Colon> int => bit => int)
+              ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
               (bit.B0::bit))))
         n))"
   by (import prob_extra POW_HALF_POS)
@@ -165,17 +165,17 @@
            ((op <=::real => real => bool)
              ((op ^::real => nat => real)
                ((op /::real => real => real) (1::real)
-                 ((number_of::bin => real)
-                   ((op BIT::bin => bit => bin)
-                     ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+                 ((number_of \<Colon> int => real)
+                   ((op BIT \<Colon> int => bit => int)
+                     ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
                        (bit.B1::bit))
                      (bit.B0::bit))))
                n)
              ((op ^::real => nat => real)
                ((op /::real => real => real) (1::real)
-                 ((number_of::bin => real)
-                   ((op BIT::bin => bit => bin)
-                     ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+                 ((number_of \<Colon> int => real)
+                   ((op BIT \<Colon> int => bit => int)
+                     ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
                        (bit.B1::bit))
                      (bit.B0::bit))))
                m))))"
@@ -186,21 +186,21 @@
      (op =::real => real => bool)
       ((op ^::real => nat => real)
         ((op /::real => real => real) (1::real)
-          ((number_of::bin => real)
-            ((op BIT::bin => bit => bin)
-              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+          ((number_of \<Colon> int => real)
+            ((op BIT \<Colon> int => bit => int)
+              ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
               (bit.B0::bit))))
         n)
       ((op *::real => real => real)
-        ((number_of::bin => real)
-          ((op BIT::bin => bit => bin)
-            ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+        ((number_of \<Colon> int => real)
+          ((op BIT \<Colon> int => bit => int)
+            ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
             (bit.B0::bit)))
         ((op ^::real => nat => real)
           ((op /::real => real => real) (1::real)
-            ((number_of::bin => real)
-              ((op BIT::bin => bit => bin)
-                ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+            ((number_of \<Colon> int => real)
+              ((op BIT \<Colon> int => bit => int)
+                ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
                   (bit.B1::bit))
                 (bit.B0::bit))))
           ((Suc::nat => nat) n))))"
@@ -227,22 +227,22 @@
 lemma ONE_MINUS_HALF: "(op =::real => real => bool)
  ((op -::real => real => real) (1::real)
    ((op /::real => real => real) (1::real)
-     ((number_of::bin => real)
-       ((op BIT::bin => bit => bin)
-         ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+     ((number_of \<Colon> int => real)
+       ((op BIT \<Colon> int => bit => int)
+         ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
          (bit.B0::bit)))))
  ((op /::real => real => real) (1::real)
-   ((number_of::bin => real)
-     ((op BIT::bin => bit => bin)
-       ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+   ((number_of \<Colon> int => real)
+     ((op BIT \<Colon> int => bit => int)
+       ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
        (bit.B0::bit))))"
   by (import prob_extra ONE_MINUS_HALF)
 
 lemma HALF_LT_1: "(op <::real => real => bool)
  ((op /::real => real => real) (1::real)
-   ((number_of::bin => real)
-     ((op BIT::bin => bit => bin)
-       ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+   ((number_of \<Colon> int => real)
+     ((op BIT \<Colon> int => bit => int)
+       ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
        (bit.B0::bit))))
  (1::real)"
   by (import prob_extra HALF_LT_1)
@@ -252,17 +252,17 @@
      (op =::real => real => bool)
       ((op ^::real => nat => real)
         ((op /::real => real => real) (1::real)
-          ((number_of::bin => real)
-            ((op BIT::bin => bit => bin)
-              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+          ((number_of \<Colon> int => real)
+            ((op BIT \<Colon> int => bit => int)
+              ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
               (bit.B0::bit))))
         n)
       ((inverse::real => real)
         ((real::nat => real)
           ((op ^::nat => nat => nat)
-            ((number_of::bin => nat)
-              ((op BIT::bin => bit => bin)
-                ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+            ((number_of \<Colon> int => nat)
+              ((op BIT \<Colon> int => bit => int)
+                ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
                   (bit.B1::bit))
                 (bit.B0::bit)))
             n))))"
@@ -1405,27 +1405,27 @@
       ((op +::real => real => real)
         ((op ^::real => nat => real)
           ((op /::real => real => real) (1::real)
-            ((number_of::bin => real)
-              ((op BIT::bin => bit => bin)
-                ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+            ((number_of \<Colon> int => real)
+              ((op BIT \<Colon> int => bit => int)
+                ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
                   (bit.B1::bit))
                 (bit.B0::bit))))
           ((size::bool list => nat)
             ((SNOC::bool => bool list => bool list) (True::bool) l)))
         ((op ^::real => nat => real)
           ((op /::real => real => real) (1::real)
-            ((number_of::bin => real)
-              ((op BIT::bin => bit => bin)
-                ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+            ((number_of \<Colon> int => real)
+              ((op BIT \<Colon> int => bit => int)
+                ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
                   (bit.B1::bit))
                 (bit.B0::bit))))
           ((size::bool list => nat)
             ((SNOC::bool => bool list => bool list) (False::bool) l))))
       ((op ^::real => nat => real)
         ((op /::real => real => real) (1::real)
-          ((number_of::bin => real)
-            ((op BIT::bin => bit => bin)
-              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+          ((number_of \<Colon> int => real)
+            ((op BIT \<Colon> int => bit => int)
+              ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
               (bit.B0::bit))))
         ((size::bool list => nat) l)))"
   by (import prob ALG_TWINS_MEASURE)
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Import/HOL/HOL4Real.thy
--- a/src/HOL/Import/HOL/HOL4Real.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Import/HOL/HOL4Real.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -525,9 +525,9 @@
       ((op <=::real => real => bool) (1::real) x)
       ((op <=::real => real => bool) (1::real)
         ((op ^::real => nat => real) x
-          ((number_of::bin => nat)
-            ((op BIT::bin => bit => bin)
-              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+          ((number_of \<Colon> int => nat)
+            ((op BIT \<Colon> int => bit => int)
+              ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
               (bit.B0::bit))))))"
   by (import real REAL_LE1_POW2)
 
@@ -537,9 +537,9 @@
       ((op <::real => real => bool) (1::real) x)
       ((op <::real => real => bool) (1::real)
         ((op ^::real => nat => real) x
-          ((number_of::bin => nat)
-            ((op BIT::bin => bit => bin)
-              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+          ((number_of \<Colon> int => nat)
+            ((op BIT \<Colon> int => bit => int)
+              ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
               (bit.B0::bit))))))"
   by (import real REAL_LT1_POW2)
 
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Import/HOL/HOL4Vec.thy
--- a/src/HOL/Import/HOL/HOL4Vec.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Import/HOL/HOL4Vec.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -1282,9 +1282,9 @@
  (%x::nat.
      (op -->::bool => bool => bool)
       ((op <::nat => nat => bool) x
-        ((number_of::bin => nat)
-          ((op BIT::bin => bit => bin)
-            ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+        ((number_of \<Colon> int => nat)
+          ((op BIT \<Colon> int => bit => int)
+            ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
             (bit.B0::bit))))
       ((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x))
         x))"
@@ -1499,10 +1499,10 @@
                                  k (0::nat) w2)))
                            ((BV::bool => nat) cin))
                          ((op ^::nat => nat => nat)
-                           ((number_of::bin => nat)
-                             ((op BIT::bin => bit => bin)
-                               ((op BIT::bin => bit => bin)
-                                 (Numeral.Pls::bin) (bit.B1::bit))
+                           ((number_of \<Colon> int => nat)
+                             ((op BIT \<Colon> int => bit => int)
+                               ((op BIT \<Colon> int => bit => int)
+                                 (Numeral.Pls \<Colon> int) (bit.B1::bit))
                                (bit.B0::bit)))
                            k)))))))"
   by (import bword_arith ACARRY_EQ_ADD_DIV)
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Import/HOL/HOL4Word32.thy
--- a/src/HOL/Import/HOL/HOL4Word32.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Import/HOL/HOL4Word32.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -116,9 +116,9 @@
  (%n::nat.
      (op <::nat => nat => bool) (0::nat)
       ((op ^::nat => nat => nat)
-        ((number_of::bin => nat)
-          ((op BIT::bin => bit => bin)
-            ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+        ((number_of \<Colon> int => nat)
+          ((op BIT \<Colon> int => bit => int)
+            ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
             (bit.B0::bit)))
         n))"
   by (import bits ZERO_LT_TWOEXP)
@@ -136,16 +136,16 @@
           (op -->::bool => bool => bool) ((op <::nat => nat => bool) a b)
            ((op <::nat => nat => bool)
              ((op ^::nat => nat => nat)
-               ((number_of::bin => nat)
-                 ((op BIT::bin => bit => bin)
-                   ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+               ((number_of \<Colon> int => nat)
+                 ((op BIT \<Colon> int => bit => int)
+                   ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
                      (bit.B1::bit))
                    (bit.B0::bit)))
                a)
              ((op ^::nat => nat => nat)
-               ((number_of::bin => nat)
-                 ((op BIT::bin => bit => bin)
-                   ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+               ((number_of \<Colon> int => nat)
+                 ((op BIT \<Colon> int => bit => int)
+                   ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
                      (bit.B1::bit))
                    (bit.B0::bit)))
                b))))"
@@ -158,16 +158,16 @@
           (op -->::bool => bool => bool) ((op <=::nat => nat => bool) a b)
            ((op <=::nat => nat => bool)
              ((op ^::nat => nat => nat)
-               ((number_of::bin => nat)
-                 ((op BIT::bin => bit => bin)
-                   ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+               ((number_of \<Colon> int => nat)
+                 ((op BIT \<Colon> int => bit => int)
+                   ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
                      (bit.B1::bit))
                    (bit.B0::bit)))
                a)
              ((op ^::nat => nat => nat)
-               ((number_of::bin => nat)
-                 ((op BIT::bin => bit => bin)
-                   ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+               ((number_of \<Colon> int => nat)
+                 ((op BIT \<Colon> int => bit => int)
+                   ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
                      (bit.B1::bit))
                    (bit.B0::bit)))
                b))))"
@@ -179,16 +179,16 @@
       (%b::nat.
           (op <=::nat => nat => bool)
            ((op ^::nat => nat => nat)
-             ((number_of::bin => nat)
-               ((op BIT::bin => bit => bin)
-                 ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+             ((number_of \<Colon> int => nat)
+               ((op BIT \<Colon> int => bit => int)
+                 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
                    (bit.B1::bit))
                  (bit.B0::bit)))
              ((op -::nat => nat => nat) a b))
            ((op ^::nat => nat => nat)
-             ((number_of::bin => nat)
-               ((op BIT::bin => bit => bin)
-                 ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+             ((number_of \<Colon> int => nat)
+               ((op BIT \<Colon> int => bit => int)
+                 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
                    (bit.B1::bit))
                  (bit.B0::bit)))
              a)))"
@@ -348,24 +348,24 @@
              (%x::nat.
                  (op =::nat => nat => bool)
                   ((op ^::nat => nat => nat)
-                    ((number_of::bin => nat)
-                      ((op BIT::bin => bit => bin)
-                        ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+                    ((number_of \<Colon> int => nat)
+                      ((op BIT \<Colon> int => bit => int)
+                        ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
                           (bit.B1::bit))
                         (bit.B0::bit)))
                     b)
                   ((op *::nat => nat => nat)
                     ((op ^::nat => nat => nat)
-                      ((number_of::bin => nat)
-                        ((op BIT::bin => bit => bin)
-                          ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+                      ((number_of \<Colon> int => nat)
+                        ((op BIT \<Colon> int => bit => int)
+                          ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
                             (bit.B1::bit))
                           (bit.B0::bit)))
                       ((op +::nat => nat => nat) x (1::nat)))
                     ((op ^::nat => nat => nat)
-                      ((number_of::bin => nat)
-                        ((op BIT::bin => bit => bin)
-                          ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+                      ((number_of \<Colon> int => nat)
+                        ((op BIT \<Colon> int => bit => int)
+                          ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
                             (bit.B1::bit))
                           (bit.B0::bit)))
                       a))))))"
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/IntArith.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -20,7 +20,7 @@
   int :: number ..
 
 defs (overloaded)
-  int_number_of_def: "(number_of w :: int) == of_int (Rep_Bin w)"
+  int_number_of_def: "(number_of w :: int) == of_int w"
     --{*the type constraint is essential!*}
 
 instance int :: number_ring
@@ -365,12 +365,9 @@
 subsection {* code generator setup *}
 
 code_typename
-  "Numeral.bin" "IntDef.bin"
   "Numeral.bit" "IntDef.bit"
 
 code_constname
-  "Numeral.Abs_Bin" "IntDef.bin"
-  "Numeral.Rep_Bin" "IntDef.int_of_bin"
   "Numeral.Pls" "IntDef.pls"
   "Numeral.Min" "IntDef.min"
   "Numeral.Bit" "IntDef.bit"
@@ -387,36 +384,29 @@
 lemma
   Numeral_Bit_refl [code fun]: "Numeral.Bit = Numeral.Bit" ..
 
-lemma
-  number_of_is_rep_bin [code inline]: "number_of = Rep_Bin"
-proof
-  fix b
-  show "number_of b = Rep_Bin b" 
-  unfolding int_number_of_def by simp
-qed
+lemma zero_is_num_zero [code fun, code inline]:
+  "(0::int) = Numeral.Pls" 
+  unfolding Pls_def ..
 
-lemma zero_is_num_zero [code, code inline]:
-  "(0::int) = Rep_Bin Numeral.Pls" 
-  unfolding Pls_def Abs_Bin_inverse' ..
+lemma one_is_num_one [code fun, code inline]:
+  "(1::int) = Numeral.Pls BIT bit.B1" 
+  unfolding Pls_def Bit_def by simp 
 
-lemma one_is_num_one [code, code inline]:
-  "(1::int) = Rep_Bin (Numeral.Pls BIT bit.B1)" 
-  unfolding Pls_def Bit_def Abs_Bin_inverse' by simp 
+lemma number_of_is_id [code fun, code inline]:
+  "number_of (k::int) = k"
+  unfolding int_number_of_def by simp
 
-lemma negate_bin_minus:
-  "(Rep_Bin b :: int) = - Rep_Bin (bin_minus b)"
-  unfolding bin_minus_def Abs_Bin_inverse' by simp
-
-lemmas [code inline] =
-  bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
-  bin_pred_Pls  bin_pred_Min  bin_pred_1  bin_pred_0
+lemma number_of_minus:
+  "number_of (b :: int) = (- number_of (- b) :: int)"
+  unfolding int_number_of_def by simp
 
 ML {*
 structure Numeral =
 struct
 
-val negate_bin_minus_thm = eq_reflection OF [thm "negate_bin_minus"];
-val number_of_is_rep_bin_thm = eq_reflection OF [thm "number_of_is_rep_bin"];
+val number_of_minus_thm = eq_reflection OF [thm "number_of_minus"];
+val minus_rewrites = map (fn thm => eq_reflection OF [thm])
+  [minus_1, minus_0, minus_Pls, minus_Min, pred_1, pred_0, pred_Pls, pred_Min];
 
 fun int_of_numeral thy num = HOLogic.dest_binum num
   handle TERM _
@@ -424,7 +414,6 @@
 
 fun elim_negate thy thms =
   let
-    val thms' = map (CodegenTheorems.rewrite_fun [number_of_is_rep_bin_thm]) thms;
     fun bins_of (Const _) =
           I
       | bins_of (Var _) =
@@ -437,28 +426,32 @@
           bins_of t
       | bins_of (t as _ $ _) =
           case strip_comb t
-           of (Const ("Numeral.Rep_Bin", _), [bin]) => cons bin
+           of (Const ("Numeral.Bit", _), _) => cons t
             | (t', ts) => bins_of t' #> fold bins_of ts;
-    fun is_negative bin = case try HOLogic.dest_binum bin
+    fun is_negative num = case try HOLogic.dest_binum num
      of SOME i => i < 0
       | _ => false;
     fun instantiate_with bin =
-      Drule.instantiate' [] [(SOME o cterm_of thy) bin] negate_bin_minus_thm;
+      Drule.instantiate' [] [(SOME o cterm_of thy) bin] number_of_minus_thm;
     val rewrites  =
       []
-      |> fold (bins_of o prop_of) thms'
+      |> fold (bins_of o prop_of) thms
       |> filter is_negative
       |> map instantiate_with
-  in if null rewrites then thms' else
-    map (CodegenTheorems.rewrite_fun rewrites) thms'
+  in if null rewrites then thms else
+    map (CodegenTheorems.rewrite_fun (rewrites @ minus_rewrites)) thms
   end;
 
 end;
 *}
 
+code_const "Numeral.Pls" and "Numeral.Min"
+  (SML target_atom "(0 : IntInf.int)" and target_atom "(~1 : IntInf.int)")
+  (Haskell target_atom "0" and target_atom "(negate ~1)")
+
 setup {*
   CodegenTheorems.add_preproc Numeral.elim_negate
-  #> CodegenPackage.add_appconst ("Numeral.Rep_Bin", CodegenPackage.appgen_rep_bin Numeral.int_of_numeral)
+  #> CodegenPackage.add_appconst ("Numeral.Bit", CodegenPackage.appgen_rep_bin Numeral.int_of_numeral)
 *}
 
 
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -935,7 +935,7 @@
       Type ("fun", [_, Type ("nat", [])])) $ bin) =
         SOME (Codegen.invoke_codegen thy defs s thyname b (gr,
           Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
-            (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin)))
+            (Const ("Numeral.number_of", HOLogic.intT --> HOLogic.intT) $ bin)))
   | number_of_codegen _ _ _ _ _ _ _ = NONE;
 *}
 
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/IntDiv.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -9,7 +9,7 @@
 header{*The Division Operators div and mod; the Divides Relation dvd*}
 
 theory IntDiv
-imports SetInterval Recdef
+imports "../SetInterval" "../Recdef"
 uses ("IntDiv_setup.ML")
 begin
 
@@ -959,7 +959,7 @@
           (if b=bit.B0 | (0::int) \<le> number_of w                    
            then number_of v div (number_of w)     
            else (number_of v + (1::int)) div (number_of w))"
-apply (simp only: number_of_eq Bin_simps UNIV_I split: split_if) 
+apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if) 
 apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac 
             split: bit.split)
 done
@@ -1001,7 +1001,7 @@
         | bit.B1 => if (0::int) \<le> number_of w  
                 then 2 * (number_of v mod number_of w) + 1     
                 else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
-apply (simp only: number_of_eq Bin_simps UNIV_I split: bit.split) 
+apply (simp only: number_of_eq numeral_simps UNIV_I split: bit.split) 
 apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
                  not_0_le_lemma neg_zmod_mult_2 add_ac)
 done
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -17,8 +17,7 @@
 instance nat :: number ..
 
 defs (overloaded)
-  nat_number_of_def:
-  "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
+  nat_number_of_def: "number_of v == nat (number_of (v\<Colon>int))"
 
 abbreviation (xsymbols)
   square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999)
@@ -113,14 +112,14 @@
 
 lemma Suc_nat_number_of_add:
      "Suc (number_of v + n) =  
-        (if neg (number_of v :: int) then 1+n else number_of (bin_succ v) + n)" 
+        (if neg (number_of v :: int) then 1+n else number_of (succ v) + n)" 
 by (simp del: nat_number_of 
          add: nat_number_of_def neg_nat
               Suc_nat_eq_nat_zadd1 number_of_succ) 
 
 lemma Suc_nat_number_of [simp]:
      "Suc (number_of v) =  
-        (if neg (number_of v :: int) then 1 else number_of (bin_succ v))"
+        (if neg (number_of v :: int) then 1 else number_of (succ v))"
 apply (cut_tac n = 0 in Suc_nat_number_of_add)
 apply (simp cong del: if_weak_cong)
 done
@@ -133,7 +132,7 @@
      "(number_of v :: nat) + number_of v' =  
          (if neg (number_of v :: int) then number_of v'  
           else if neg (number_of v' :: int) then number_of v  
-          else number_of (bin_add v v'))"
+          else number_of (v + v'))"
 by (force dest!: neg_nat
           simp del: nat_number_of
           simp add: nat_number_of_def nat_add_distrib [symmetric]) 
@@ -152,7 +151,7 @@
 lemma diff_nat_number_of [simp]: 
      "(number_of v :: nat) - number_of v' =  
         (if neg (number_of v' :: int) then number_of v  
-         else let d = number_of (bin_add v (bin_minus v')) in     
+         else let d = number_of (v + uminus v') in     
               if neg d then 0 else nat d)"
 by (simp del: nat_number_of add: diff_nat_eq_if nat_number_of_def) 
 
@@ -162,7 +161,7 @@
 
 lemma mult_nat_number_of [simp]:
      "(number_of v :: nat) * number_of v' =  
-       (if neg (number_of v :: int) then 0 else number_of (bin_mult v v'))"
+       (if neg (number_of v :: int) then 0 else number_of (v * v'))"
 by (force dest!: neg_nat
           simp del: nat_number_of
           simp add: nat_number_of_def nat_mult_distrib [symmetric]) 
@@ -246,7 +245,7 @@
      "((number_of v :: nat) = number_of v') =  
       (if neg (number_of v :: int) then (iszero (number_of v' :: int) | neg (number_of v' :: int))  
        else if neg (number_of v' :: int) then iszero (number_of v :: int)  
-       else iszero (number_of (bin_add v (bin_minus v')) :: int))"
+       else iszero (number_of (v + uminus v') :: int))"
 apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
                   eq_nat_nat_iff eq_number_of_eq nat_0 iszero_def
             split add: split_if cong add: imp_cong)
@@ -260,13 +259,11 @@
 (*"neg" is used in rewrite rules for binary comparisons*)
 lemma less_nat_number_of [simp]:
      "((number_of v :: nat) < number_of v') =  
-         (if neg (number_of v :: int) then neg (number_of (bin_minus v') :: int)  
-          else neg (number_of (bin_add v (bin_minus v')) :: int))"
+         (if neg (number_of v :: int) then neg (number_of (uminus v') :: int)  
+          else neg (number_of (v + uminus v') :: int))"
 by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
                 nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless
-         cong add: imp_cong, simp) 
-
-
+         cong add: imp_cong, simp add: Pls_def)
 
 
 (*Maps #n to n for n = 0, 1, 2*)
@@ -437,8 +434,8 @@
 by (rule trans [OF eq_sym_conv eq_number_of_0])
 
 lemma less_0_number_of [simp]:
-     "((0::nat) < number_of v) = neg (number_of (bin_minus v) :: int)"
-by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
+     "((0::nat) < number_of v) = neg (number_of (uminus v) :: int)"
+by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] Pls_def)
 
 
 lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
@@ -450,7 +447,7 @@
 
 lemma eq_number_of_Suc [simp]:
      "(number_of v = Suc n) =  
-        (let pv = number_of (bin_pred v) in  
+        (let pv = number_of (pred v) in  
          if neg pv then False else nat pv = n)"
 apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
                   number_of_pred nat_number_of_def 
@@ -461,13 +458,13 @@
 
 lemma Suc_eq_number_of [simp]:
      "(Suc n = number_of v) =  
-        (let pv = number_of (bin_pred v) in  
+        (let pv = number_of (pred v) in  
          if neg pv then False else nat pv = n)"
 by (rule trans [OF eq_sym_conv eq_number_of_Suc])
 
 lemma less_number_of_Suc [simp]:
      "(number_of v < Suc n) =  
-        (let pv = number_of (bin_pred v) in  
+        (let pv = number_of (pred v) in  
          if neg pv then True else nat pv < n)"
 apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
                   number_of_pred nat_number_of_def  
@@ -478,7 +475,7 @@
 
 lemma less_Suc_number_of [simp]:
      "(Suc n < number_of v) =  
-        (let pv = number_of (bin_pred v) in  
+        (let pv = number_of (pred v) in  
          if neg pv then False else n < nat pv)"
 apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
                   number_of_pred nat_number_of_def
@@ -489,13 +486,13 @@
 
 lemma le_number_of_Suc [simp]:
      "(number_of v <= Suc n) =  
-        (let pv = number_of (bin_pred v) in  
+        (let pv = number_of (pred v) in  
          if neg pv then True else nat pv <= n)"
 by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
 
 lemma le_Suc_number_of [simp]:
      "(Suc n <= number_of v) =  
-        (let pv = number_of (bin_pred v) in  
+        (let pv = number_of (pred v) in  
          if neg pv then False else n <= nat pv)"
 by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
 
@@ -568,23 +565,20 @@
 text{*For the integers*}
 
 lemma zpower_number_of_even:
-     "(z::int) ^ number_of (w BIT bit.B0) =  
-      (let w = z ^ (number_of w) in  w*w)"
-apply (simp del: nat_number_of  add: nat_number_of_def number_of_BIT Let_def)
-apply (simp only: number_of_add) 
+  "(z::int) ^ number_of (w BIT bit.B0) = (let w = z ^ (number_of w) in w * w)"
+unfolding Let_def nat_number_of_def number_of_BIT bit.cases
 apply (rule_tac x = "number_of w" in spec, clarify)
 apply (case_tac " (0::int) <= x")
 apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
 done
 
 lemma zpower_number_of_odd:
-     "(z::int) ^ number_of (w BIT bit.B1) =  
-          (if (0::int) <= number_of w                    
-           then (let w = z ^ (number_of w) in  z*w*w)    
-           else 1)"
-apply (simp del: nat_number_of  add: nat_number_of_def number_of_BIT Let_def)
-apply (simp only: number_of_add nat_numeral_1_eq_1 not_neg_eq_ge_0 neg_eq_less_0) 
-apply (rule_tac x = "number_of w" in spec, clarify)
+  "(z::int) ^ number_of (w BIT bit.B1) = (if (0::int) <= number_of w                    
+     then (let w = z ^ (number_of w) in z * w * w) else 1)"
+unfolding Let_def nat_number_of_def number_of_BIT bit.cases
+apply (rule_tac x = "number_of w" in spec, auto)
+apply (simp only: nat_add_distrib nat_mult_distrib)
+apply simp
 apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat)
 done
 
@@ -695,13 +689,13 @@
      "number_of v + (number_of v' + (k::nat)) =  
          (if neg (number_of v :: int) then number_of v' + k  
           else if neg (number_of v' :: int) then number_of v + k  
-          else number_of (bin_add v v') + k)"
+          else number_of (v + v') + k)"
 by simp
 
 lemma nat_number_of_mult_left:
      "number_of v * (number_of v' * (k::nat)) =  
          (if neg (number_of v :: int) then 0
-          else number_of (bin_mult v v') * k)"
+          else number_of (v * v') * k)"
 by simp
 
 
@@ -780,7 +774,7 @@
 subsection {* code generator setup *}
 
 lemma number_of_is_nat_rep_bin [code inline]:
-  "(number_of b :: nat) = nat (Rep_Bin b)"
+  "(number_of b :: nat) = nat (number_of b)"
   unfolding nat_number_of_def int_number_of_def by simp
 
 
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Integ/NatSimprocs.thy
--- a/src/HOL/Integ/NatSimprocs.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/NatSimprocs.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -22,9 +22,9 @@
 text {*Now just instantiating @{text n} to @{text "number_of v"} does
   the right simplification, but with some redundant inequality
   tests.*}
-lemma neg_number_of_bin_pred_iff_0:
-     "neg (number_of (bin_pred v)::int) = (number_of v = (0::nat))"
-apply (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0) ")
+lemma neg_number_of_pred_iff_0:
+  "neg (number_of (pred v)::int) = (number_of v = (0::nat))"
+apply (subgoal_tac "neg (number_of (pred v)) = (number_of v < Suc 0) ")
 apply (simp only: less_Suc_eq_le le_0_eq)
 apply (subst less_number_of_Suc, simp)
 done
@@ -32,13 +32,13 @@
 text{*No longer required as a simprule because of the @{text inverse_fold}
    simproc*}
 lemma Suc_diff_number_of:
-     "neg (number_of (bin_minus v)::int) ==>  
-      Suc m - (number_of v) = m - (number_of (bin_pred v))"
+     "neg (number_of (uminus v)::int) ==>  
+      Suc m - (number_of v) = m - (number_of (pred v))"
 apply (subst Suc_diff_eq_diff_pred)
 apply simp
 apply (simp del: nat_numeral_1_eq_1)
 apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric] 
-                        neg_number_of_bin_pred_iff_0)
+                        neg_number_of_pred_iff_0)
 done
 
 lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
@@ -49,40 +49,40 @@
 
 lemma nat_case_number_of [simp]:
      "nat_case a f (number_of v) =  
-        (let pv = number_of (bin_pred v) in  
+        (let pv = number_of (pred v) in  
          if neg pv then a else f (nat pv))"
-by (simp split add: nat.split add: Let_def neg_number_of_bin_pred_iff_0)
+by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
 
 lemma nat_case_add_eq_if [simp]:
      "nat_case a f ((number_of v) + n) =  
-       (let pv = number_of (bin_pred v) in  
+       (let pv = number_of (pred v) in  
          if neg pv then nat_case a f n else f (nat pv + n))"
 apply (subst add_eq_if)
 apply (simp split add: nat.split
             del: nat_numeral_1_eq_1
 	    add: numeral_1_eq_Suc_0 [symmetric] Let_def 
-                 neg_imp_number_of_eq_0 neg_number_of_bin_pred_iff_0)
+                 neg_imp_number_of_eq_0 neg_number_of_pred_iff_0)
 done
 
 lemma nat_rec_number_of [simp]:
      "nat_rec a f (number_of v) =  
-        (let pv = number_of (bin_pred v) in  
+        (let pv = number_of (pred v) in  
          if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
 apply (case_tac " (number_of v) ::nat")
-apply (simp_all (no_asm_simp) add: Let_def neg_number_of_bin_pred_iff_0)
+apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
 apply (simp split add: split_if_asm)
 done
 
 lemma nat_rec_add_eq_if [simp]:
      "nat_rec a f (number_of v + n) =  
-        (let pv = number_of (bin_pred v) in  
+        (let pv = number_of (pred v) in  
          if neg pv then nat_rec a f n  
                    else f (nat pv + n) (nat_rec a f (nat pv + n)))"
 apply (subst add_eq_if)
 apply (simp split add: nat.split
             del: nat_numeral_1_eq_1
             add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0
-                 neg_number_of_bin_pred_iff_0)
+                 neg_number_of_pred_iff_0)
 done
 
 
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Integ/Numeral.thy
--- a/src/HOL/Integ/Numeral.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/Numeral.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -1,292 +1,315 @@
-(*  Title:	HOL/Integ/Numeral.thy
+(*  Title:      HOL/Integ/Numeral.thy
     ID:         $Id$
-    Author:	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright	1994  University of Cambridge
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
 *)
 
-header{*Arithmetic on Binary Integers*}
+header {* Arithmetic on Binary Integers *}
 
 theory Numeral
 imports IntDef Datatype
 uses "../Tools/numeral_syntax.ML"
 begin
 
-text{*This formalization defines binary arithmetic in terms of the integers
-rather than using a datatype. This avoids multiple representations (leading
-zeroes, etc.)  See @{text "ZF/Integ/twos-compl.ML"}, function @{text
-int_of_binary}, for the numerical interpretation.
+text {*
+  This formalization defines binary arithmetic in terms of the integers
+  rather than using a datatype. This avoids multiple representations (leading
+  zeroes, etc.)  See @{text "ZF/Integ/twos-compl.ML"}, function @{text
+  int_of_binary}, for the numerical interpretation.
 
-The representation expects that @{text "(m mod 2)"} is 0 or 1,
-even if m is negative;
-For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
-@{text "-5 = (-3)*2 + 1"}.
+  The representation expects that @{text "(m mod 2)"} is 0 or 1,
+  even if m is negative;
+  For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
+  @{text "-5 = (-3)*2 + 1"}.
 *}
 
+text{*
+  This datatype avoids the use of type @{typ bool}, which would make
+  all of the rewrite rules higher-order.
+*}
 
-typedef (Bin)
-  bin = "UNIV::int set"
-    by (auto)
-
-text{*This datatype avoids the use of type @{typ bool}, which would make
-all of the rewrite rules higher-order. If the use of datatype causes
-problems, this two-element type can easily be formalized using typedef.*}
 datatype bit = B0 | B1
 
 constdefs
-  Pls :: "bin"
-   "Pls == Abs_Bin 0"
-
-  Min :: "bin"
-   "Min == Abs_Bin (- 1)"
-
-  Bit :: "[bin,bit] => bin"    (infixl "BIT" 90)
-   --{*That is, 2w+b*}
-   "w BIT b == Abs_Bin ((case b of B0 => 0 | B1 => 1) + Rep_Bin w + Rep_Bin w)"
-
+  Pls :: int
+  "Pls == 0"
+  Min :: int
+  "Min == - 1"
+  Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90)
+  "k BIT b == (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
 
 axclass
   number < type  -- {* for numeric types: nat, int, real, \dots *}
 
 consts
-  number_of :: "bin => 'a::number"
+  number_of :: "int \<Rightarrow> 'a::number"
 
 syntax
-  "_Numeral" :: "num_const => 'a"    ("_")
+  "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
 
 setup NumeralSyntax.setup
 
 abbreviation
-  "Numeral0 == number_of Pls"
-  "Numeral1 == number_of (Pls BIT B1)"
+  "Numeral0 \<equiv> number_of Pls"
+  "Numeral1 \<equiv> number_of (Pls BIT B1)"
 
-lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
+lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
   -- {* Unfold all @{text let}s involving constants *}
-  by (simp add: Let_def)
+  unfolding Let_def ..
+
+lemma Let_0 [simp]: "Let 0 f = f 0"
+  unfolding Let_def ..
+
+lemma Let_1 [simp]: "Let 1 f = f 1"
+  unfolding Let_def ..
 
-lemma Let_0 [simp]: "Let 0 f == f 0"
-  by (simp add: Let_def)
+definition
+  succ :: "int \<Rightarrow> int"
+  "succ k = k + 1"
+  pred :: "int \<Rightarrow> int"
+  "pred k = k - 1"
+
+lemmas numeral_simps = 
+  succ_def pred_def Pls_def Min_def Bit_def
 
-lemma Let_1 [simp]: "Let 1 f == f 1"
-  by (simp add: Let_def)
+text {* Removal of leading zeroes *}
+
+lemma Pls_0_eq [simp]:
+  "Pls BIT B0 = Pls"
+  unfolding numeral_simps by simp
+
+lemma Min_1_eq [simp]:
+  "Min BIT B1 = Min"
+  unfolding numeral_simps by simp
 
 
-constdefs
-  bin_succ  :: "bin=>bin"
-   "bin_succ w == Abs_Bin(Rep_Bin w + 1)"
-
-  bin_pred  :: "bin=>bin"
-   "bin_pred w == Abs_Bin(Rep_Bin w - 1)"
+subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}
 
-  bin_minus  :: "bin=>bin"
-   "bin_minus w == Abs_Bin(- (Rep_Bin w))"
+lemma succ_Pls [simp]:
+  "succ Pls = Pls BIT B1"
+  unfolding numeral_simps by simp
 
-  bin_add  :: "[bin,bin]=>bin"
-   "bin_add v w == Abs_Bin(Rep_Bin v + Rep_Bin w)"
-
-  bin_mult  :: "[bin,bin]=>bin"
-   "bin_mult v w == Abs_Bin(Rep_Bin v * Rep_Bin w)"
+lemma succ_Min [simp]:
+  "succ Min = Pls"
+  unfolding numeral_simps by simp
 
-lemma Abs_Bin_inverse':
-  "Rep_Bin (Abs_Bin x) = x"
-by (rule Abs_Bin_inverse) (auto simp add: Bin_def)
-
-lemmas Bin_simps = 
-       bin_succ_def bin_pred_def bin_minus_def bin_add_def bin_mult_def
-       Pls_def Min_def Bit_def Abs_Bin_inverse Rep_Bin_inverse Bin_def
+lemma succ_1 [simp]:
+  "succ (k BIT B1) = succ k BIT B0"
+  unfolding numeral_simps by simp
 
-text{*Removal of leading zeroes*}
-lemma Pls_0_eq [simp]: "Pls BIT B0 = Pls"
-by (simp add: Bin_simps)
+lemma succ_0 [simp]:
+  "succ (k BIT B0) = k BIT B1"
+  unfolding numeral_simps by simp
 
-lemma Min_1_eq [simp]: "Min BIT B1 = Min"
-by (simp add: Bin_simps)
-
-subsection{*The Functions @{term bin_succ},  @{term bin_pred} and @{term bin_minus}*}
+lemma pred_Pls [simp]:
+  "pred Pls = Min"
+  unfolding numeral_simps by simp
 
-lemma bin_succ_Pls [simp]: "bin_succ Pls = Pls BIT B1"
-by (simp add: Bin_simps) 
-
-lemma bin_succ_Min [simp]: "bin_succ Min = Pls"
-by (simp add: Bin_simps) 
-
-lemma bin_succ_1 [simp]: "bin_succ(w BIT B1) = (bin_succ w) BIT B0"
-by (simp add: Bin_simps add_ac) 
+lemma pred_Min [simp]:
+  "pred Min = Min BIT B0"
+  unfolding numeral_simps by simp
 
-lemma bin_succ_0 [simp]: "bin_succ(w BIT B0) = w BIT B1"
-by (simp add: Bin_simps add_ac) 
+lemma pred_1 [simp]:
+  "pred (k BIT B1) = k BIT B0"
+  unfolding numeral_simps by simp
 
-lemma bin_pred_Pls [simp]: "bin_pred Pls = Min"
-by (simp add: Bin_simps) 
-
-lemma bin_pred_Min [simp]: "bin_pred Min = Min BIT B0"
-by (simp add: Bin_simps diff_minus) 
+lemma pred_0 [simp]:
+  "pred (k BIT B0) = pred k BIT B1"
+  unfolding numeral_simps by simp 
 
-lemma bin_pred_1 [simp]: "bin_pred(w BIT B1) = w BIT B0"
-by (simp add: Bin_simps) 
+lemma minus_Pls [simp]:
+  "- Pls = Pls"
+  unfolding numeral_simps by simp 
 
-lemma bin_pred_0 [simp]: "bin_pred(w BIT B0) = (bin_pred w) BIT B1"
-by (simp add: Bin_simps diff_minus add_ac) 
-
-lemma bin_minus_Pls [simp]: "bin_minus Pls = Pls"
-by (simp add: Bin_simps) 
+lemma minus_Min [simp]:
+  "- Min = Pls BIT B1"
+  unfolding numeral_simps by simp 
 
-lemma bin_minus_Min [simp]: "bin_minus Min = Pls BIT B1"
-by (simp add: Bin_simps) 
+lemma minus_1 [simp]:
+  "- (k BIT B1) = pred (- k) BIT B1"
+  unfolding numeral_simps by simp 
 
-lemma bin_minus_1 [simp]:
-     "bin_minus (w BIT B1) = bin_pred (bin_minus w) BIT B1"
-by (simp add: Bin_simps add_ac diff_minus) 
-
- lemma bin_minus_0 [simp]: "bin_minus(w BIT B0) = (bin_minus w) BIT B0"
-by (simp add: Bin_simps) 
+lemma minus_0 [simp]:
+  "- (k BIT B0) = (- k) BIT B0"
+  unfolding numeral_simps by simp 
 
 
-subsection{*Binary Addition and Multiplication:
-         @{term bin_add} and @{term bin_mult}*}
+subsection {*
+  Binary Addition and Multiplication: @{term "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
+    and @{term "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
+*}
 
-lemma bin_add_Pls [simp]: "bin_add Pls w = w"
-by (simp add: Bin_simps) 
+lemma add_Pls [simp]:
+  "Pls + k = k"
+  unfolding numeral_simps by simp 
 
-lemma bin_add_Min [simp]: "bin_add Min w = bin_pred w"
-by (simp add: Bin_simps diff_minus add_ac) 
+lemma add_Min [simp]:
+  "Min + k = pred k"
+  unfolding numeral_simps by simp
 
-lemma bin_add_BIT_11 [simp]:
-     "bin_add (v BIT B1) (w BIT B1) = bin_add v (bin_succ w) BIT B0"
-by (simp add: Bin_simps add_ac)
+lemma add_BIT_11 [simp]:
+  "(k BIT B1) + (l BIT B1) = (k + succ l) BIT B0"
+  unfolding numeral_simps by simp
 
-lemma bin_add_BIT_10 [simp]:
-     "bin_add (v BIT B1) (w BIT B0) = (bin_add v w) BIT B1"
-by (simp add: Bin_simps add_ac)
+lemma add_BIT_10 [simp]:
+  "(k BIT B1) + (l BIT B0) = (k + l) BIT B1"
+  unfolding numeral_simps by simp
 
-lemma bin_add_BIT_0 [simp]:
-     "bin_add (v BIT B0) (w BIT y) = bin_add v w BIT y"
-by (simp add: Bin_simps add_ac)
+lemma add_BIT_0 [simp]:
+  "(k BIT B0) + (l BIT b) = (k + l) BIT b"
+  unfolding numeral_simps by simp 
 
-lemma bin_add_Pls_right [simp]: "bin_add w Pls = w"
-by (simp add: Bin_simps) 
+lemma add_Pls_right [simp]:
+  "k + Pls = k"
+  unfolding numeral_simps by simp 
 
-lemma bin_add_Min_right [simp]: "bin_add w Min = bin_pred w"
-by (simp add: Bin_simps diff_minus) 
+lemma add_Min_right [simp]:
+  "k + Min = pred k"
+  unfolding numeral_simps by simp 
 
-lemma bin_mult_Pls [simp]: "bin_mult Pls w = Pls"
-by (simp add: Bin_simps) 
+lemma mult_Pls [simp]:
+  "Pls * w = Pls"
+  unfolding numeral_simps by simp 
 
-lemma bin_mult_Min [simp]: "bin_mult Min w = bin_minus w"
-by (simp add: Bin_simps) 
+lemma mult_Min [simp]:
+  "Min * k = - k"
+  unfolding numeral_simps by simp 
 
-lemma bin_mult_1 [simp]:
-     "bin_mult (v BIT B1) w = bin_add ((bin_mult v w) BIT B0) w"
-by (simp add: Bin_simps add_ac left_distrib)
+lemma mult_num1 [simp]:
+  "(k BIT B1) * l = ((k * l) BIT B0) + l"
+  unfolding numeral_simps int_distrib by simp 
 
-lemma bin_mult_0 [simp]: "bin_mult (v BIT B0) w = (bin_mult v w) BIT B0"
-by (simp add: Bin_simps left_distrib)
+lemma mult_num0 [simp]:
+  "(k BIT B0) * l = (k * l) BIT B0"
+  unfolding numeral_simps int_distrib by simp 
 
 
 
-subsection{*Converting Numerals to Rings: @{term number_of}*}
+subsection {* Converting Numerals to Rings: @{term number_of} *}
 
 axclass number_ring \<subseteq> number, comm_ring_1
-  number_of_eq: "number_of w = of_int (Rep_Bin w)"
+  number_of_eq: "number_of k = of_int k"
 
 lemma number_of_succ:
-     "number_of(bin_succ w) = (1 + number_of w ::'a::number_ring)"
-by (simp add: number_of_eq Bin_simps)
+  "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
+  unfolding number_of_eq numeral_simps by simp
 
 lemma number_of_pred:
-     "number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)"
-by (simp add: number_of_eq Bin_simps)
+  "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"
+  unfolding number_of_eq numeral_simps by simp
 
 lemma number_of_minus:
-     "number_of(bin_minus w) = (- (number_of w)::'a::number_ring)"
-by (simp add: number_of_eq Bin_simps) 
+  "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
+  unfolding number_of_eq numeral_simps by simp
 
 lemma number_of_add:
-     "number_of(bin_add v w) = (number_of v + number_of w::'a::number_ring)"
-by (simp add: number_of_eq Bin_simps) 
+  "number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
+  unfolding number_of_eq numeral_simps by simp
 
 lemma number_of_mult:
-     "number_of(bin_mult v w) = (number_of v * number_of w::'a::number_ring)"
-by (simp add: number_of_eq Bin_simps) 
+  "number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
+  unfolding number_of_eq numeral_simps by simp
 
-text{*The correctness of shifting.  But it doesn't seem to give a measurable
-  speed-up.*}
+text {*
+  The correctness of shifting.
+  But it doesn't seem to give a measurable speed-up.
+*}
+
 lemma double_number_of_BIT:
-     "(1+1) * number_of w = (number_of (w BIT B0) ::'a::number_ring)"
-by (simp add: number_of_eq Bin_simps left_distrib) 
+  "(1 + 1) * number_of w = (number_of (w BIT B0) ::'a::number_ring)"
+  unfolding number_of_eq numeral_simps left_distrib by simp
 
-text{*Converting numerals 0 and 1 to their abstract versions*}
-lemma numeral_0_eq_0 [simp]: "Numeral0 = (0::'a::number_ring)"
-by (simp add: number_of_eq Bin_simps) 
+text {*
+  Converting numerals 0 and 1 to their abstract versions.
+*}
+
+lemma numeral_0_eq_0 [simp]:
+  "Numeral0 = (0::'a::number_ring)"
+  unfolding number_of_eq numeral_simps by simp
 
-lemma numeral_1_eq_1 [simp]: "Numeral1 = (1::'a::number_ring)"
-by (simp add: number_of_eq Bin_simps) 
+lemma numeral_1_eq_1 [simp]:
+  "Numeral1 = (1::'a::number_ring)"
+  unfolding number_of_eq numeral_simps by simp
 
-text{*Special-case simplification for small constants*}
+text {*
+  Special-case simplification for small constants.
+*}
 
-text{*Unary minus for the abstract constant 1. Cannot be inserted
-  as a simprule until later: it is @{text number_of_Min} re-oriented!*}
-lemma numeral_m1_eq_minus_1: "(-1::'a::number_ring) = - 1"
-by (simp add: number_of_eq Bin_simps) 
-
+text{*
+  Unary minus for the abstract constant 1. Cannot be inserted
+  as a simprule until later: it is @{text number_of_Min} re-oriented!
+*}
 
-lemma mult_minus1 [simp]: "-1 * z = -(z::'a::number_ring)"
-by (simp add: numeral_m1_eq_minus_1)
+lemma numeral_m1_eq_minus_1:
+  "(-1::'a::number_ring) = - 1"
+  unfolding number_of_eq numeral_simps by simp
 
-lemma mult_minus1_right [simp]: "z * -1 = -(z::'a::number_ring)"
-by (simp add: numeral_m1_eq_minus_1)
+lemma mult_minus1 [simp]:
+  "-1 * z = -(z::'a::number_ring)"
+  unfolding number_of_eq numeral_simps by simp
+
+lemma mult_minus1_right [simp]:
+  "z * -1 = -(z::'a::number_ring)"
+  unfolding number_of_eq numeral_simps by simp
 
 (*Negation of a coefficient*)
 lemma minus_number_of_mult [simp]:
-     "- (number_of w) * z = number_of(bin_minus w) * (z::'a::number_ring)"
-by (simp add: number_of_minus)
+   "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"
+   unfolding number_of_eq by simp
+
+text {* Subtraction *}
+
+lemma diff_number_of_eq:
+  "number_of v - number_of w =
+    (number_of (v + uminus w)::'a::number_ring)"
+  unfolding number_of_eq by simp
 
-text{*Subtraction*}
-lemma diff_number_of_eq:
-     "number_of v - number_of w =
-      (number_of(bin_add v (bin_minus w))::'a::number_ring)"
-by (simp add: diff_minus number_of_add number_of_minus)
+lemma number_of_Pls:
+  "number_of Pls = (0::'a::number_ring)"
+  unfolding number_of_eq numeral_simps by simp
+
+lemma number_of_Min:
+  "number_of Min = (- 1::'a::number_ring)"
+  unfolding number_of_eq numeral_simps by simp
+
+lemma number_of_BIT:
+  "number_of(w BIT x) = (case x of B0 => 0 | B1 => (1::'a::number_ring))
+    + (number_of w) + (number_of w)"
+  unfolding number_of_eq numeral_simps by (simp split: bit.split)
 
 
-lemma number_of_Pls: "number_of Pls = (0::'a::number_ring)"
-by (simp add: number_of_eq Bin_simps) 
-
-lemma number_of_Min: "number_of Min = (- 1::'a::number_ring)"
-by (simp add: number_of_eq Bin_simps) 
+subsection {* Equality of Binary Numbers *}
 
-lemma number_of_BIT:
-     "number_of(w BIT x) = (case x of B0 => 0 | B1 => (1::'a::number_ring)) +
-	                   (number_of w) + (number_of w)"
-by (simp add: number_of_eq Bin_simps split: bit.split) 
-
-
-
-subsection{*Equality of Binary Numbers*}
-
-text{*First version by Norbert Voelker*}
+text {* First version by Norbert Voelker *}
 
 lemma eq_number_of_eq:
   "((number_of x::'a::number_ring) = number_of y) =
-   iszero (number_of (bin_add x (bin_minus y)) :: 'a)"
-by (simp add: iszero_def compare_rls number_of_add number_of_minus)
+   iszero (number_of (x + uminus y) :: 'a)"
+  unfolding iszero_def number_of_add number_of_minus
+  by (simp add: compare_rls)
 
-lemma iszero_number_of_Pls: "iszero ((number_of Pls)::'a::number_ring)"
-by (simp add: iszero_def numeral_0_eq_0)
+lemma iszero_number_of_Pls:
+  "iszero ((number_of Pls)::'a::number_ring)"
+  unfolding iszero_def numeral_0_eq_0 ..
 
-lemma nonzero_number_of_Min: "~ iszero ((number_of Min)::'a::number_ring)"
-by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)
+lemma nonzero_number_of_Min:
+  "~ iszero ((number_of Min)::'a::number_ring)"
+  unfolding iszero_def numeral_m1_eq_minus_1 by simp
 
 
-subsection{*Comparisons, for Ordered Rings*}
+subsection {* Comparisons, for Ordered Rings *}
 
-lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_idom))"
+lemma double_eq_0_iff:
+  "(a + a = 0) = (a = (0::'a::ordered_idom))"
 proof -
-  have "a + a = (1+1)*a" by (simp add: left_distrib)
+  have "a + a = (1 + 1) * a" unfolding left_distrib by simp
   with zero_less_two [where 'a = 'a]
   show ?thesis by force
 qed
 
 lemma le_imp_0_less: 
-  assumes le: "0 \<le> z" shows "(0::int) < 1 + z"
+  assumes le: "0 \<le> z"
+  shows "(0::int) < 1 + z"
 proof -
   have "0 \<le> z" .
   also have "... < z + 1" by (rule less_add_one) 
@@ -294,7 +317,8 @@
   finally show "0 < 1 + z" .
 qed
 
-lemma odd_nonzero: "1 + z + z \<noteq> (0::int)";
+lemma odd_nonzero:
+  "1 + z + z \<noteq> (0::int)";
 proof (cases z rule: int_cases)
   case (nonneg n)
   have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
@@ -315,11 +339,13 @@
   qed
 qed
 
+text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
 
-text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
-lemma Ints_odd_nonzero: "a \<in> Ints ==> 1 + a + a \<noteq> (0::'a::ordered_idom)"
-proof (unfold Ints_def) 
-  assume "a \<in> range of_int"
+lemma Ints_odd_nonzero:
+  assumes in_Ints: "a \<in> Ints"
+  shows "1 + a + a \<noteq> (0::'a::ordered_idom)"
+proof -
+  from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   then obtain z where a: "a = of_int z" ..
   show ?thesis
   proof
@@ -330,46 +356,50 @@
   qed
 qed 
 
-lemma Ints_number_of: "(number_of w :: 'a::number_ring) \<in> Ints"
-by (simp add: number_of_eq Ints_def) 
-
+lemma Ints_number_of:
+  "(number_of w :: 'a::number_ring) \<in> Ints"
+  unfolding number_of_eq Ints_def by simp
 
 lemma iszero_number_of_BIT:
-     "iszero (number_of (w BIT x)::'a) = 
-      (x=B0 & iszero (number_of w::'a::{ordered_idom,number_ring}))"
-by (simp add: iszero_def number_of_eq Bin_simps double_eq_0_iff 
-              Ints_odd_nonzero Ints_def split: bit.split)
+  "iszero (number_of (w BIT x)::'a) = 
+   (x = B0 \<and> iszero (number_of w::'a::{ordered_idom,number_ring}))"
+  by (simp add: iszero_def number_of_eq numeral_simps double_eq_0_iff 
+    Ints_odd_nonzero Ints_def split: bit.split)
 
 lemma iszero_number_of_0:
-     "iszero (number_of (w BIT B0) :: 'a::{ordered_idom,number_ring}) = 
-      iszero (number_of w :: 'a)"
-by (simp only: iszero_number_of_BIT simp_thms)
+  "iszero (number_of (w BIT B0) :: 'a::{ordered_idom,number_ring}) = 
+  iszero (number_of w :: 'a)"
+  by (simp only: iszero_number_of_BIT simp_thms)
 
 lemma iszero_number_of_1:
-     "~ iszero (number_of (w BIT B1)::'a::{ordered_idom,number_ring})"
-by (simp add: iszero_number_of_BIT) 
+  "~ iszero (number_of (w BIT B1)::'a::{ordered_idom,number_ring})"
+  by (simp add: iszero_number_of_BIT) 
 
 
-subsection{*The Less-Than Relation*}
+subsection {* The Less-Than Relation *}
 
 lemma less_number_of_eq_neg:
-    "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
-     = neg (number_of (bin_add x (bin_minus y)) :: 'a)"
+  "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
+  = neg (number_of (x + uminus y) :: 'a)"
 apply (subst less_iff_diff_less_0) 
 apply (simp add: neg_def diff_minus number_of_add number_of_minus)
 done
 
-text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
-  @{term Numeral0} IS @{term "number_of Pls"} *}
+text {*
+  If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
+  @{term Numeral0} IS @{term "number_of Pls"}
+*}
+
 lemma not_neg_number_of_Pls:
-     "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
-by (simp add: neg_def numeral_0_eq_0)
+  "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
+  by (simp add: neg_def numeral_0_eq_0)
 
 lemma neg_number_of_Min:
-     "neg (number_of Min ::'a::{ordered_idom,number_ring})"
-by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
+  "neg (number_of Min ::'a::{ordered_idom,number_ring})"
+  by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
 
-lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))"
+lemma double_less_0_iff:
+  "(a + a < 0) = (a < (0::'a::ordered_idom))"
 proof -
   have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
   also have "... = (a < 0)"
@@ -378,7 +408,8 @@
   finally show ?thesis .
 qed
 
-lemma odd_less_0: "(1 + z + z < 0) = (z < (0::int))";
+lemma odd_less_0:
+  "(1 + z + z < 0) = (z < (0::int))";
 proof (cases z rule: int_cases)
   case (nonneg n)
   thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
@@ -386,14 +417,16 @@
 next
   case (neg n)
   thus ?thesis by (simp del: int_Suc
-			add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
+    add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
 qed
 
-text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
+text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
+
 lemma Ints_odd_less_0: 
-     "a \<in> Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))";
-proof (unfold Ints_def) 
-  assume "a \<in> range of_int"
+  assumes in_Ints: "a \<in> Ints"
+  shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))";
+proof -
+  from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   then obtain z where a: "a = of_int z" ..
   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
     by (simp add: a)
@@ -403,93 +436,98 @@
 qed
 
 lemma neg_number_of_BIT:
-     "neg (number_of (w BIT x)::'a) = 
-      neg (number_of w :: 'a::{ordered_idom,number_ring})"
-by (simp add: neg_def number_of_eq Bin_simps double_less_0_iff
-              Ints_odd_less_0 Ints_def split: bit.split)
-
+  "neg (number_of (w BIT x)::'a) = 
+  neg (number_of w :: 'a::{ordered_idom,number_ring})"
+  by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff
+    Ints_odd_less_0 Ints_def split: bit.split)
 
-text{*Less-Than or Equals*}
+text {* Less-Than or Equals *}
+
+text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
 
-text{*Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals*}
 lemmas le_number_of_eq_not_less =
-       linorder_not_less [of "number_of w" "number_of v", symmetric, 
-                          standard]
+  linorder_not_less [of "number_of w" "number_of v", symmetric, 
+  standard]
 
 lemma le_number_of_eq:
     "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
-     = (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))"
+     = (~ (neg (number_of (y + uminus x) :: 'a)))"
 by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
 
 
-text{*Absolute value (@{term abs})*}
+text {* Absolute value (@{term abs}) *}
 
 lemma abs_number_of:
-     "abs(number_of x::'a::{ordered_idom,number_ring}) =
-      (if number_of x < (0::'a) then -number_of x else number_of x)"
-by (simp add: abs_if)
+  "abs(number_of x::'a::{ordered_idom,number_ring}) =
+   (if number_of x < (0::'a) then -number_of x else number_of x)"
+  by (simp add: abs_if)
 
 
-text{*Re-orientation of the equation nnn=x*}
-lemma number_of_reorient: "(number_of w = x) = (x = number_of w)"
-by auto
+text {* Re-orientation of the equation nnn=x *}
 
-
+lemma number_of_reorient:
+  "(number_of w = x) = (x = number_of w)"
+  by auto
 
 
-subsection{*Simplification of arithmetic operations on integer constants.*}
+subsection {* Simplification of arithmetic operations on integer constants. *}
 
-lemmas bin_arith_extra_simps = 
-       number_of_add [symmetric]
-       number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
-       number_of_mult [symmetric]
-       diff_number_of_eq abs_number_of 
+lemmas arith_extra_simps = 
+  number_of_add [symmetric]
+  number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
+  number_of_mult [symmetric]
+  diff_number_of_eq abs_number_of 
+
+text {*
+  For making a minimal simpset, one must include these default simprules.
+  Also include @{text simp_thms}.
+*}
 
-text{*For making a minimal simpset, one must include these default simprules.
-  Also include @{text simp_thms} *}
-lemmas bin_arith_simps = 
-       Numeral.bit.distinct
-       Pls_0_eq Min_1_eq
-       bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
-       bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
-       bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
-       bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
-       bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0 
-       bin_add_Pls_right bin_add_Min_right
-       abs_zero abs_one bin_arith_extra_simps
+lemmas arith_simps = 
+  bit.distinct
+  Pls_0_eq Min_1_eq
+  pred_Pls pred_Min pred_1 pred_0
+  succ_Pls succ_Min succ_1 succ_0
+  add_Pls add_Min add_BIT_0 add_BIT_10 add_BIT_11
+  minus_Pls minus_Min minus_1 minus_0
+  mult_Pls mult_Min mult_num1 mult_num0 
+  add_Pls_right add_Min_right
+  abs_zero abs_one arith_extra_simps
 
-text{*Simplification of relational operations*}
-lemmas bin_rel_simps = 
-       eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
-       iszero_number_of_0 iszero_number_of_1
-       less_number_of_eq_neg
-       not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
-       neg_number_of_Min neg_number_of_BIT
-       le_number_of_eq
+text {* Simplification of relational operations *}
 
-declare bin_arith_extra_simps [simp]
-declare bin_rel_simps [simp]
+lemmas rel_simps = 
+  eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
+  iszero_number_of_0 iszero_number_of_1
+  less_number_of_eq_neg
+  not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
+  neg_number_of_Min neg_number_of_BIT
+  le_number_of_eq
+
+declare arith_extra_simps [simp]
+declare rel_simps [simp]
 
 
-subsection{*Simplification of arithmetic when nested to the right*}
+subsection {* Simplification of arithmetic when nested to the right. *}
 
 lemma add_number_of_left [simp]:
-     "number_of v + (number_of w + z) =
-      (number_of(bin_add v w) + z::'a::number_ring)"
-by (simp add: add_assoc [symmetric])
+  "number_of v + (number_of w + z) =
+   (number_of(v + w) + z::'a::number_ring)"
+  by (simp add: add_assoc [symmetric])
 
 lemma mult_number_of_left [simp]:
-    "number_of v * (number_of w * z) =
-     (number_of(bin_mult v w) * z::'a::number_ring)"
-by (simp add: mult_assoc [symmetric])
+  "number_of v * (number_of w * z) =
+   (number_of(v * w) * z::'a::number_ring)"
+  by (simp add: mult_assoc [symmetric])
 
 lemma add_number_of_diff1:
-    "number_of v + (number_of w - c) = 
-     number_of(bin_add v w) - (c::'a::number_ring)"
-by (simp add: diff_minus add_number_of_left)
+  "number_of v + (number_of w - c) = 
+  number_of(v + w) - (c::'a::number_ring)"
+  by (simp add: diff_minus add_number_of_left)
 
-lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) =
-     number_of (bin_add v (bin_minus w)) + (c::'a::number_ring)"
+lemma add_number_of_diff2 [simp]:
+  "number_of v + (c - number_of w) =
+   number_of (v + uminus w) + (c::'a::number_ring)"
 apply (subst diff_number_of_eq [symmetric])
 apply (simp only: compare_rls)
 done
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Integ/Presburger.thy
--- a/src/HOL/Integ/Presburger.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/Presburger.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -992,7 +992,8 @@
 lemma not_true_eq_false: "(~ True) = False" by simp
 
 
-lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)"
+lemma int_eq_number_of_eq:
+  "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
   by simp
 lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)" 
   by (simp only: iszero_number_of_Pls)
@@ -1006,7 +1007,7 @@
 lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)" 
   by simp
 
-lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)"
+lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
   by simp
 
 lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))" 
@@ -1018,18 +1019,20 @@
 lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
   by simp
 
-lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (bin_add y (bin_minus x)))::int))"
+lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
   by simp
-lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (bin_add v w)"
+lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
   by simp
 
-lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (bin_add v (bin_minus w))"
+lemma int_number_of_diff_sym:
+  "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
   by simp
 
-lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (bin_mult v w)"
+lemma int_number_of_mult_sym:
+  "((number_of v)::int) * number_of w = number_of (v * w)"
   by simp
 
-lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (bin_minus v)"
+lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
   by simp
 lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
   by simp
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Wed Sep 06 13:48:02 2006 +0200
@@ -7,90 +7,90 @@
 
 (** Misc ML bindings **)
 
-val bin_succ_Pls = thm"bin_succ_Pls";
-val bin_succ_Min = thm"bin_succ_Min";
-val bin_succ_1 = thm"bin_succ_1";
-val bin_succ_0 = thm"bin_succ_0";
+val succ_Pls = thm "succ_Pls";
+val succ_Min = thm "succ_Min";
+val succ_1 = thm "succ_1";
+val succ_0 = thm "succ_0";
 
-val bin_pred_Pls = thm"bin_pred_Pls";
-val bin_pred_Min = thm"bin_pred_Min";
-val bin_pred_1 = thm"bin_pred_1";
-val bin_pred_0 = thm"bin_pred_0";
+val pred_Pls = thm "pred_Pls";
+val pred_Min = thm "pred_Min";
+val pred_1 = thm "pred_1";
+val pred_0 = thm "pred_0";
 
-val bin_minus_Pls = thm"bin_minus_Pls";
-val bin_minus_Min = thm"bin_minus_Min";
-val bin_minus_1 = thm"bin_minus_1";
-val bin_minus_0 = thm"bin_minus_0";
+val minus_Pls = thm "minus_Pls";
+val minus_Min = thm "minus_Min";
+val minus_1 = thm "minus_1";
+val minus_0 = thm "minus_0";
 
-val bin_add_Pls = thm"bin_add_Pls";
-val bin_add_Min = thm"bin_add_Min";
-val bin_add_BIT_11 = thm"bin_add_BIT_11";
-val bin_add_BIT_10 = thm"bin_add_BIT_10";
-val bin_add_BIT_0 = thm"bin_add_BIT_0";
-val bin_add_Pls_right = thm"bin_add_Pls_right";
-val bin_add_Min_right = thm"bin_add_Min_right";
+val add_Pls = thm "add_Pls";
+val add_Min = thm "add_Min";
+val add_BIT_11 = thm "add_BIT_11";
+val add_BIT_10 = thm "add_BIT_10";
+val add_BIT_0 = thm "add_BIT_0";
+val add_Pls_right = thm "add_Pls_right";
+val add_Min_right = thm "add_Min_right";
 
-val bin_mult_Pls = thm"bin_mult_Pls";
-val bin_mult_Min = thm"bin_mult_Min";
-val bin_mult_1 = thm"bin_mult_1";
-val bin_mult_0 = thm"bin_mult_0";
+val mult_Pls = thm "mult_Pls";
+val mult_Min = thm "mult_Min";
+val mult_num1 = thm "mult_num1";
+val mult_num0 = thm "mult_num0";
 
 val neg_def = thm "neg_def";
 val iszero_def = thm "iszero_def";
 
-val number_of_succ = thm"number_of_succ";
-val number_of_pred = thm"number_of_pred";
-val number_of_minus = thm"number_of_minus";
-val number_of_add = thm"number_of_add";
-val diff_number_of_eq = thm"diff_number_of_eq";
-val number_of_mult = thm"number_of_mult";
-val double_number_of_BIT = thm"double_number_of_BIT";
-val numeral_0_eq_0 = thm"numeral_0_eq_0";
-val numeral_1_eq_1 = thm"numeral_1_eq_1";
-val numeral_m1_eq_minus_1 = thm"numeral_m1_eq_minus_1";
-val mult_minus1 = thm"mult_minus1";
-val mult_minus1_right = thm"mult_minus1_right";
-val minus_number_of_mult = thm"minus_number_of_mult";
-val zero_less_nat_eq = thm"zero_less_nat_eq";
-val eq_number_of_eq = thm"eq_number_of_eq";
-val iszero_number_of_Pls = thm"iszero_number_of_Pls";
-val nonzero_number_of_Min = thm"nonzero_number_of_Min";
-val iszero_number_of_BIT = thm"iszero_number_of_BIT";
-val iszero_number_of_0 = thm"iszero_number_of_0";
-val iszero_number_of_1 = thm"iszero_number_of_1";
-val less_number_of_eq_neg = thm"less_number_of_eq_neg";
-val le_number_of_eq = thm"le_number_of_eq";
-val not_neg_number_of_Pls = thm"not_neg_number_of_Pls";
-val neg_number_of_Min = thm"neg_number_of_Min";
-val neg_number_of_BIT = thm"neg_number_of_BIT";
-val le_number_of_eq_not_less = thm"le_number_of_eq_not_less";
-val abs_number_of = thm"abs_number_of";
-val number_of_reorient = thm"number_of_reorient";
-val add_number_of_left = thm"add_number_of_left";
-val mult_number_of_left = thm"mult_number_of_left";
-val add_number_of_diff1 = thm"add_number_of_diff1";
-val add_number_of_diff2 = thm"add_number_of_diff2";
-val less_iff_diff_less_0 = thm"less_iff_diff_less_0";
-val eq_iff_diff_eq_0 = thm"eq_iff_diff_eq_0";
-val le_iff_diff_le_0 = thm"le_iff_diff_le_0";
+val number_of_succ = thm "number_of_succ";
+val number_of_pred = thm "number_of_pred";
+val number_of_minus = thm "number_of_minus";
+val number_of_add = thm "number_of_add";
+val diff_number_of_eq = thm "diff_number_of_eq";
+val number_of_mult = thm "number_of_mult";
+val double_number_of_BIT = thm "double_number_of_BIT";
+val numeral_0_eq_0 = thm "numeral_0_eq_0";
+val numeral_1_eq_1 = thm "numeral_1_eq_1";
+val numeral_m1_eq_minus_1 = thm "numeral_m1_eq_minus_1";
+val mult_minus1 = thm "mult_minus1";
+val mult_minus1_right = thm "mult_minus1_right";
+val minus_number_of_mult = thm "minus_number_of_mult";
+val zero_less_nat_eq = thm "zero_less_nat_eq";
+val eq_number_of_eq = thm "eq_number_of_eq";
+val iszero_number_of_Pls = thm "iszero_number_of_Pls";
+val nonzero_number_of_Min = thm "nonzero_number_of_Min";
+val iszero_number_of_BIT = thm "iszero_number_of_BIT";
+val iszero_number_of_0 = thm "iszero_number_of_0";
+val iszero_number_of_1 = thm "iszero_number_of_1";
+val less_number_of_eq_neg = thm "less_number_of_eq_neg";
+val le_number_of_eq = thm "le_number_of_eq";
+val not_neg_number_of_Pls = thm "not_neg_number_of_Pls";
+val neg_number_of_Min = thm "neg_number_of_Min";
+val neg_number_of_BIT = thm "neg_number_of_BIT";
+val le_number_of_eq_not_less = thm "le_number_of_eq_not_less";
+val abs_number_of = thm "abs_number_of";
+val number_of_reorient = thm "number_of_reorient";
+val add_number_of_left = thm "add_number_of_left";
+val mult_number_of_left = thm "mult_number_of_left";
+val add_number_of_diff1 = thm "add_number_of_diff1";
+val add_number_of_diff2 = thm "add_number_of_diff2";
+val less_iff_diff_less_0 = thm "less_iff_diff_less_0";
+val eq_iff_diff_eq_0 = thm "eq_iff_diff_eq_0";
+val le_iff_diff_le_0 = thm "le_iff_diff_le_0";
 
-val bin_arith_extra_simps = thms"bin_arith_extra_simps";
-val bin_arith_simps = thms"bin_arith_simps";
-val bin_rel_simps = thms"bin_rel_simps";
+val arith_extra_simps = thms "arith_extra_simps";
+val arith_simps = thms "arith_simps";
+val rel_simps = thms "rel_simps";
 
 val zless_imp_add1_zle = thm "zless_imp_add1_zle";
 
-val combine_common_factor = thm"combine_common_factor";
-val eq_add_iff1 = thm"eq_add_iff1";
-val eq_add_iff2 = thm"eq_add_iff2";
-val less_add_iff1 = thm"less_add_iff1";
-val less_add_iff2 = thm"less_add_iff2";
-val le_add_iff1 = thm"le_add_iff1";
-val le_add_iff2 = thm"le_add_iff2";
+val combine_common_factor = thm "combine_common_factor";
+val eq_add_iff1 = thm "eq_add_iff1";
+val eq_add_iff2 = thm "eq_add_iff2";
+val less_add_iff1 = thm "less_add_iff1";
+val less_add_iff2 = thm "less_add_iff2";
+val le_add_iff1 = thm "le_add_iff1";
+val le_add_iff2 = thm "le_add_iff2";
 
-val arith_special = thms"arith_special";
+val arith_special = thms "arith_special";
 
-structure Bin_Simprocs =
+structure Int_Numeral_Base_Simprocs =
   struct
   fun prove_conv tacs ctxt (_: thm list) (t, u) =
     if t aconv u then NONE
@@ -133,13 +133,13 @@
 
 
 Addsimps arith_special;
-Addsimprocs [Bin_Simprocs.reorient_simproc];
+Addsimprocs [Int_Numeral_Base_Simprocs.reorient_simproc];
 
 
 structure Int_Numeral_Simprocs =
 struct
 
-(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in simprocs
+(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in Int_Numeral_Base_Simprocs
   isn't complicated by the abstract 0 and 1.*)
 val numeral_syms = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym];
 
@@ -175,7 +175,7 @@
 
 fun numtermless tu = (numterm_ord tu = LESS);
 
-(*Defined in this file, but perhaps needed only for simprocs of type nat.*)
+(*Defined in this file, but perhaps needed only for Int_Numeral_Base_Simprocs of type nat.*)
 val num_ss = HOL_ss settermless numtermless;
 
 
@@ -273,20 +273,20 @@
 val mult_1s = thms "mult_1s";
 
 (*To perform binary arithmetic.  The "left" rewriting handles patterns
-  created by the simprocs, such as 3 * (5 * x). *)
-val bin_simps = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym,
+  created by the Int_Numeral_Base_Simprocs, such as 3 * (5 * x). *)
+val simps = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym,
                  add_number_of_left, mult_number_of_left] @
-                bin_arith_simps @ bin_rel_simps;
+                arith_simps @ rel_simps;
 
 (*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
   during re-arrangement*)
-val non_add_bin_simps =
-  subtract Thm.eq_thm [add_number_of_left, number_of_add RS sym] bin_simps;
+val non_add_simps =
+  subtract Thm.eq_thm [add_number_of_left, number_of_add RS sym] simps;
 
 (*To evaluate binary negations of coefficients*)
 val minus_simps = [numeral_m1_eq_minus_1 RS sym, number_of_minus RS sym,
-                   bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
-                   bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
+                   minus_1, minus_0, minus_Pls, minus_Min,
+                   pred_1, pred_0, pred_Pls, pred_Min];
 
 (*To let us treat subtraction as addition*)
 val diff_simps = [diff_minus, minus_add_distrib, minus_minus];
@@ -322,14 +322,14 @@
 
   val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
     diff_simps @ minus_simps @ add_ac
-  val norm_ss2 = num_ss addsimps non_add_bin_simps @ mult_minus_simps
+  val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
   val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
   fun norm_tac ss =
     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
 
-  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps
+  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
   end;
@@ -337,7 +337,7 @@
 
 structure EqCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   val bal_add1 = eq_add_iff1 RS trans
@@ -346,7 +346,7 @@
 
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binrel "Orderings.less"
   val dest_bal = HOLogic.dest_bin "Orderings.less" Term.dummyT
   val bal_add1 = less_add_iff1 RS trans
@@ -355,7 +355,7 @@
 
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binrel "Orderings.less_eq"
   val dest_bal = HOLogic.dest_bin "Orderings.less_eq" Term.dummyT
   val bal_add1 = le_add_iff1 RS trans
@@ -363,7 +363,7 @@
 );
 
 val cancel_numerals =
-  map Bin_Simprocs.prep_simproc
+  map Int_Numeral_Base_Simprocs.prep_simproc
    [("inteq_cancel_numerals",
      ["(l::'a::number_ring) + m = n",
       "(l::'a::number_ring) = m + n",
@@ -398,19 +398,19 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff 1
   val left_distrib      = combine_common_factor RS trans
-  val prove_conv        = Bin_Simprocs.prove_conv_nohyps
+  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
   val trans_tac         = fn _ => trans_tac
 
   val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
     diff_simps @ minus_simps @ add_ac
-  val norm_ss2 = num_ss addsimps non_add_bin_simps @ mult_minus_simps
+  val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
   val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
   fun norm_tac ss =
     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
 
-  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps
+  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
   end;
@@ -418,7 +418,7 @@
 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
 
 val combine_numerals =
-  Bin_Simprocs.prep_simproc
+  Int_Numeral_Base_Simprocs.prep_simproc
     ("int_combine_numerals", 
      ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], 
      K CombineNumerals.proc);
@@ -479,7 +479,7 @@
 structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
 
 val assoc_fold_simproc =
-  Bin_Simprocs.prep_simproc
+  Int_Numeral_Base_Simprocs.prep_simproc
    ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
     K Semiring_Times_Assoc.proc);
 
@@ -503,10 +503,10 @@
 
 (* reduce contradictory <= to False *)
 val add_rules =
-    simp_thms @ bin_arith_simps @ bin_rel_simps @ arith_special @
+    simp_thms @ arith_simps @ rel_simps @ arith_special @
     [neg_le_iff_le, numeral_0_eq_0, numeral_1_eq_1,
      minus_zero, diff_minus, left_minus, right_minus,
-     mult_zero_left, mult_zero_right, mult_1, mult_1_right,
+     mult_zero_left, mult_zero_right, mult_num1, mult_1_right,
      minus_mult_left RS sym, minus_mult_right RS sym,
      minus_add_distrib, minus_minus, mult_assoc,
      of_nat_0, of_nat_1, of_nat_Suc, of_nat_add, of_nat_mult,
@@ -515,7 +515,7 @@
 val nat_inj_thms = [zle_int RS iffD2,
                     int_int_eq RS iffD2]
 
-val simprocs = [assoc_fold_simproc, Int_Numeral_Simprocs.combine_numerals]@
+val Int_Numeral_Base_Simprocs = [assoc_fold_simproc, Int_Numeral_Simprocs.combine_numerals]@
                Int_Numeral_Simprocs.cancel_numerals
 
 in
@@ -528,7 +528,7 @@
     lessD = lessD @ [zless_imp_add1_zle],
     neqE = neqE,
     simpset = simpset addsimps add_rules
-                      addsimprocs simprocs
+                      addsimprocs Int_Numeral_Base_Simprocs
                       addcongs [if_weak_cong]}) #>
   arith_inj_const ("NatArith.of_nat", HOLogic.natT --> HOLogic.intT) #>
   arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT) #>
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Integ/int_factor_simprocs.ML
--- a/src/HOL/Integ/int_factor_simprocs.ML	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/int_factor_simprocs.ML	Wed Sep 06 13:48:02 2006 +0200
@@ -45,25 +45,25 @@
   val trans_tac         = fn _ => trans_tac
 
   val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
-  val norm_ss2 = HOL_ss addsimps bin_simps@mult_minus_simps
+  val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
   val norm_ss3 = HOL_ss addsimps mult_ac
   fun norm_tac ss =
     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
 
-  val numeral_simp_ss = HOL_ss addsimps rel_number_of @ bin_simps
+  val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps
   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq = 
 	Int_Numeral_Simprocs.simplify_meta_eq
 	     [add_0, add_0_right,
-	      mult_zero_left, mult_zero_right, mult_1, mult_1_right];
+	      mult_zero_left, mult_zero_right, mult_num1, mult_1_right];
   end
 
 (*Version for integer division*)
 structure DivCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binop "Divides.op div"
   val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
   val cancel = int_mult_div_cancel1 RS trans
@@ -73,7 +73,7 @@
 (*Version for fields*)
 structure FieldDivCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binop "HOL.divide"
   val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
   val cancel = mult_divide_cancel_left RS trans
@@ -83,7 +83,7 @@
 (*Version for ordered rings: mult_cancel_left requires an ordering*)
 structure EqCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   val cancel = mult_cancel_left RS trans
@@ -93,7 +93,7 @@
 (*Version for (unordered) fields*)
 structure FieldEqCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   val cancel = field_mult_cancel_left RS trans
@@ -102,7 +102,7 @@
 
 structure LessCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binrel "Orderings.less"
   val dest_bal = HOLogic.dest_bin "Orderings.less" Term.dummyT
   val cancel = mult_less_cancel_left RS trans
@@ -111,7 +111,7 @@
 
 structure LeCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binrel "Orderings.less_eq"
   val dest_bal = HOLogic.dest_bin "Orderings.less_eq" Term.dummyT
   val cancel = mult_le_cancel_left RS trans
@@ -119,7 +119,7 @@
 )
 
 val ring_cancel_numeral_factors =
-  map Bin_Simprocs.prep_simproc
+  map Int_Numeral_Base_Simprocs.prep_simproc
    [("ring_eq_cancel_numeral_factor",
      ["(l::'a::{ordered_idom,number_ring}) * m = n",
       "(l::'a::{ordered_idom,number_ring}) = m * n"],
@@ -138,7 +138,7 @@
 
 
 val field_cancel_numeral_factors =
-  map Bin_Simprocs.prep_simproc
+  map Int_Numeral_Base_Simprocs.prep_simproc
    [("field_eq_cancel_numeral_factor",
      ["(l::'a::{field,number_ring}) * m = n",
       "(l::'a::{field,number_ring}) = m * n"],
@@ -261,7 +261,7 @@
   rat_arith.ML works for all fields.*)
 structure EqCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
   val simplify_meta_eq  = cancel_simplify_meta_eq mult_cancel_left
@@ -271,14 +271,14 @@
   rat_arith.ML works for all fields, using real division (/).*)
 structure DivideCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binop "Divides.op div"
   val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
   val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj
 );
 
 val int_cancel_factor =
-  map Bin_Simprocs.prep_simproc
+  map Int_Numeral_Base_Simprocs.prep_simproc
    [("ring_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"],
     K EqCancelFactor.proc),
     ("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m*n)"],
@@ -288,7 +288,7 @@
 
 structure FieldEqCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   val simplify_meta_eq  = cancel_simplify_meta_eq field_mult_cancel_left
@@ -296,7 +296,7 @@
 
 structure FieldDivideCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binop "HOL.divide"
   val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
   val simplify_meta_eq  = cancel_simplify_meta_eq mult_divide_cancel_eq_if
@@ -305,7 +305,7 @@
 (*The number_ring class is necessary because the simprocs refer to the
   binary number 1.  FIXME: probably they could use 1 instead.*)
 val field_cancel_factor =
-  map Bin_Simprocs.prep_simproc
+  map Int_Numeral_Base_Simprocs.prep_simproc
    [("field_eq_cancel_factor",
      ["(l::'a::{field,number_ring}) * m = n",
       "(l::'a::{field,number_ring}) = m * n"],
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML	Wed Sep 06 13:48:02 2006 +0200
@@ -64,7 +64,7 @@
       mult_nat_number_of, nat_number_of_mult_left, 
       less_nat_number_of, 
       Let_number_of, nat_number_of] @
-     bin_arith_simps @ bin_rel_simps;
+     arith_simps @ rel_simps;
 
 fun prep_simproc (name, pats, proc) =
   Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
@@ -182,7 +182,7 @@
 
 structure EqCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   val bal_add1 = nat_eq_add_iff1 RS trans
@@ -191,7 +191,7 @@
 
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binrel "Orderings.less"
   val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
   val bal_add1 = nat_less_add_iff1 RS trans
@@ -200,7 +200,7 @@
 
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binrel "Orderings.less_eq"
   val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
   val bal_add1 = nat_le_add_iff1 RS trans
@@ -209,7 +209,7 @@
 
 structure DiffCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binop "HOL.minus"
   val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT
   val bal_add1 = nat_diff_add_eq1 RS trans
@@ -251,7 +251,7 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
   val left_distrib      = left_add_mult_distrib RS trans
-  val prove_conv        = Bin_Simprocs.prove_conv_nohyps
+  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
   val trans_tac         = fn _ => trans_tac
 
   val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [Suc_eq_add_numeral_1] @ add_ac
@@ -293,7 +293,7 @@
 
 structure DivCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binop "Divides.op div"
   val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
   val cancel = nat_mult_div_cancel1 RS trans
@@ -302,7 +302,7 @@
 
 structure EqCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   val cancel = nat_mult_eq_cancel1 RS trans
@@ -311,7 +311,7 @@
 
 structure LessCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binrel "Orderings.less"
   val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
   val cancel = nat_mult_less_cancel1 RS trans
@@ -320,7 +320,7 @@
 
 structure LeCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binrel "Orderings.less_eq"
   val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
   val cancel = nat_mult_le_cancel1 RS trans
@@ -379,7 +379,7 @@
 
 structure EqCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_eq_cancel_disj
@@ -387,7 +387,7 @@
 
 structure LessCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binrel "Orderings.less"
   val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
   val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_less_cancel_disj
@@ -395,7 +395,7 @@
 
 structure LeCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binrel "Orderings.less_eq"
   val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
   val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_le_cancel_disj
@@ -403,7 +403,7 @@
 
 structure DivideCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binop "Divides.op div"
   val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
   val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_div_cancel_disj
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/presburger.ML	Wed Sep 06 13:48:02 2006 +0200
@@ -33,12 +33,12 @@
 val presburger_ss = simpset ();
 val binarith = map thm
   ["Pls_0_eq", "Min_1_eq",
- "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
-  "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
-  "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
-  "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", 
-  "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", 
-  "bin_add_Pls_right", "bin_add_Min_right"];
+ "pred_Pls","pred_Min","pred_1","pred_0",
+  "succ_Pls", "succ_Min", "succ_1", "succ_0",
+  "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10",
+  "add_BIT_11", "minus_Pls", "minus_Min", "minus_1", 
+  "minus_0", "mult_Pls", "mult_Min", "mult_num1", "mult_num0", 
+  "add_Pls_right", "add_Min_right"];
  val intarithrel = 
      (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
 		"int_le_number_of_eq","int_iszero_number_of_0",
@@ -116,7 +116,6 @@
 val bT = HOLogic.boolT;
 val bitT = HOLogic.bitT;
 val iT = HOLogic.intT;
-val binT = HOLogic.binT;
 val nT = HOLogic.natT;
 
 (* Allowed Consts in formulae for presburger tactic*)
@@ -162,11 +161,11 @@
 
    ("Numeral.bit.B0", bitT),
    ("Numeral.bit.B1", bitT),
-   ("Numeral.Bit", binT --> bitT --> binT),
-   ("Numeral.Pls", binT),
-   ("Numeral.Min", binT),
-   ("Numeral.number_of", binT --> iT),
-   ("Numeral.number_of", binT --> nT),
+   ("Numeral.Bit", iT --> bitT --> iT),
+   ("Numeral.Pls", iT),
+   ("Numeral.Min", iT),
+   ("Numeral.number_of", iT --> iT),
+   ("Numeral.number_of", iT --> nT),
    ("0", nT),
    ("0", iT),
    ("1", nT),
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Library/Word.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -2513,92 +2513,12 @@
 lemma "nat_to_bv (number_of Numeral.Pls) = []"
   by simp
 
-(***NO LONGER WORKS
 consts
-  fast_nat_to_bv_helper :: "bin => bit list => bit list"
+  fast_bv_to_nat_helper :: "[bit list, int] => int"
 
 primrec
-  fast_nat_to_bv_Pls: "fast_nat_to_bv_helper Numeral.Pls res = res"
-  fast_nat_to_bv_Bit: "fast_nat_to_bv_helper (w BIT b) res = fast_nat_to_bv_helper w ((if b then \<one> else \<zero>) # res)"
-
-lemma fast_nat_to_bv_def:
-  assumes pos_w: "(0::int) \<le> number_of w"
-  shows "nat_to_bv (number_of w) == norm_unsigned (fast_nat_to_bv_helper w [])"
-proof -
-  have h [rule_format]: "(0::int) \<le> number_of w ==> \<forall> l. norm_unsigned (nat_to_bv_helper (number_of w) l) = norm_unsigned (fast_nat_to_bv_helper w l)"
-  proof (induct w,simp add: nat_to_bv_helper.simps,simp)
-    fix bin b
-    assume ind: "(0::int) \<le> number_of bin ==> \<forall> l. norm_unsigned (nat_to_bv_helper (number_of bin) l) = norm_unsigned (fast_nat_to_bv_helper bin l)"
-    def qq == "number_of bin::int"
-    assume posbb: "(0::int) \<le> number_of (bin BIT b)"
-    hence indq [rule_format]: "\<forall> l. norm_unsigned (nat_to_bv_helper qq l) = norm_unsigned (fast_nat_to_bv_helper bin l)"
-      apply (unfold qq_def)
-      apply (rule ind)
-      apply simp
-      done
-    from posbb
-    have "0 \<le> qq"
-      by (simp add: qq_def)
-    with posbb
-    show "\<forall> l. norm_unsigned (nat_to_bv_helper (number_of (bin BIT b)) l) = norm_unsigned (fast_nat_to_bv_helper (bin BIT b) l)"
-      apply (subst pos_number_of)
-      apply safe
-      apply (fold qq_def)
-      apply (cases "qq = 0")
-      apply (simp add: nat_to_bv_helper.simps)
-      apply (subst indq [symmetric])
-      apply (subst indq [symmetric])
-      apply (simp add: nat_to_bv_helper.simps)
-      apply (subgoal_tac "0 < qq")
-      prefer 2
-      apply simp
-      apply simp
-      apply (subst indq [symmetric])
-      apply (subst indq [symmetric])
-      apply auto
-      apply (simp only: nat_to_bv_helper.simps [of "2 * qq + 1"])
-      apply simp
-      apply safe
-      apply (subgoal_tac "2 * qq + 1 ~= 2 * q")
-      apply simp
-      apply arith
-      apply (subgoal_tac "(2 * qq + 1) div 2 = qq")
-      apply simp
-      apply (subst zdiv_zadd1_eq,simp)
-      apply (simp only: nat_to_bv_helper.simps [of "2 * qq"])
-      apply simp
-      done
-  qed
-  from pos_w
-  have "nat_to_bv (number_of w) = norm_unsigned (nat_to_bv (number_of w))"
-    by simp
-  also have "... = norm_unsigned (fast_nat_to_bv_helper w [])"
-    apply (unfold nat_to_bv_def)
-    apply (rule h)
-    apply (rule pos_w)
-    done
-  finally show "nat_to_bv (number_of w) == norm_unsigned (fast_nat_to_bv_helper w [])"
-    by simp
-qed
-
-lemma fast_nat_to_bv_Bit0: "fast_nat_to_bv_helper (w BIT False) res = fast_nat_to_bv_helper w (\<zero> # res)"
-  by simp
-
-lemma fast_nat_to_bv_Bit1: "fast_nat_to_bv_helper (w BIT True) res = fast_nat_to_bv_helper w (\<one> # res)"
-  by simp
-
-declare fast_nat_to_bv_Bit [simp del]
-declare fast_nat_to_bv_Bit0 [simp]
-declare fast_nat_to_bv_Bit1 [simp]
-****)
-
-
-consts
-  fast_bv_to_nat_helper :: "[bit list, bin] => bin"
-
-primrec
-  fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] bin = bin"
-  fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) bin = fast_bv_to_nat_helper bs (bin BIT (bit_case bit.B0 bit.B1 b))"
+  fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
+  fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k = fast_bv_to_nat_helper bs (k BIT (bit_case bit.B0 bit.B1 b))"
 
 lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin = fast_bv_to_nat_helper bs (bin BIT bit.B0)"
   by simp
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Library/word_setup.ML
--- a/src/HOL/Library/word_setup.ML	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Library/word_setup.ML	Wed Sep 06 13:48:02 2006 +0200
@@ -27,7 +27,7 @@
 	    val fast2_th = PureThy.get_thm thy (Name "Word.fast_bv_to_nat_def")
  (*lcp**	    fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
 		if num_is_usable t
-		then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("Numeral.bin",[]))),cterm_of sg t)] fast1_th)
+		then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("IntDef.int",[]))),cterm_of sg t)] fast1_th)
 		else NONE
 	      | f _ _ _ = NONE **)
 	    fun g sg thms (Const("Word.bv_to_nat",_) $ (t as (Const("List.list.Cons",_) $ _ $ _))) =
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
--- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Wed Sep 06 13:48:02 2006 +0200
@@ -32,7 +32,7 @@
     val v_only_elem : vector -> int option
     val v_fold : ('a * (int * string) -> 'a) -> 'a -> vector -> 'a
     val m_fold : ('a * (int * vector) -> 'a) -> 'a -> matrix -> 'a
-				   
+
     val transpose_matrix : matrix -> matrix
 
     val cut_vector : int -> vector -> vector
@@ -80,53 +80,27 @@
 
 val Cons_spvec_const = Const (term_Cons, spvec_elemT --> spvecT --> spvecT)
 val Cons_spmat_const = Const (term_Cons, spmat_elemT --> spmatT --> spmatT) 
-			 
+
 val float_const = Float.float_const
 
-(*val float_const = Const (readterm "float", HOLogic.mk_prodT (HOLogic.intT, HOLogic.intT) --> HOLogic.realT)*)
-		  
 val zero = IntInf.fromInt 0
 val minus_one = IntInf.fromInt ~1
 val two = IntInf.fromInt 2
-	  
+
 val mk_intinf = Float.mk_intinf
-(*    let
-	fun mk_bit n = if n = zero then HOLogic.false_const else HOLogic.true_const
-								 
-	fun bin_of n = 
-	    if n = zero then HOLogic.pls_const
-	    else if n = minus_one then HOLogic.min_const
-	    else 
-		let 
-		    (*val (q,r) = IntInf.divMod (n, two): doesn't work in SML 10.0.7, but in newer versions!!!*)
-	            val q = IntInf.div (n, two)
-		    val r = IntInf.mod (n, two)
-		in
-		    HOLogic.bit_const $ bin_of q $ mk_bit r
-		end
-    in 
-	HOLogic.number_of_const ty $ (bin_of n)
-    end*)
 
 val mk_float  = Float.mk_float 
-(*    float_const $ (HOLogic.mk_prod ((mk_intinf HOLogic.intT a), (mk_intinf HOLogic.intT b)))*)
 
 fun float2cterm (a,b) = cterm_of sg (mk_float (a,b))
 
 fun approx_value_term prec f = Float.approx_float prec (fn (x, y) => (f x, f y))
-(*    let
-	val (flower, fupper) = ExactFloatingPoint.approx_decstr_by_bin prec value
-	val (flower, fupper) = (f flower, f fupper)
-    in
-	(mk_float flower, mk_float fupper)
-    end*)
 
 fun approx_value prec pprt value = 
-    let
-	val (flower, fupper) = approx_value_term prec pprt value			       
-    in
-	(cterm_of sg flower, cterm_of sg fupper)
-    end
+  let
+    val (flower, fupper) = approx_value_term prec pprt value
+  in
+    (cterm_of sg flower, cterm_of sg fupper)
+  end
 
 fun sign_term t = cterm_of sg t
 
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Matrix/cplex/MatrixLP.ML
--- a/src/HOL/Matrix/cplex/MatrixLP.ML	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Matrix/cplex/MatrixLP.ML	Wed Sep 06 13:48:02 2006 +0200
@@ -16,15 +16,15 @@
 structure MatrixLP : MATRIX_LP =
 struct
 
-val sg = sign_of (theory "MatrixLP")
+val thy = theory "MatrixLP";
 
-fun inst_real thm = standard (Thm.instantiate ([(ctyp_of sg (TVar (hd (term_tvars (prop_of thm)))),
-						 ctyp_of sg HOLogic.realT)], []) thm)
+fun inst_real thm = standard (Thm.instantiate ([(ctyp_of thy (TVar (hd (term_tvars (prop_of thm)))),
+						 ctyp_of thy HOLogic.realT)], []) thm)
 
 fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) = 
     let
 	val th = inst_real (thm "SparseMatrix.spm_mult_le_dual_prts_no_let")
-	fun var s x = (cterm_of sg (Var ((s,0), FloatSparseMatrixBuilder.real_spmatT)), x)
+	fun var s x = (cterm_of thy (Var ((s,0), FloatSparseMatrixBuilder.real_spmatT)), x)
 	val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, 
 				       var "r1" r1, var "r2" r2, var "b" b]) th
     in
@@ -43,8 +43,8 @@
     in
 	lp_dual_estimate_prt_primitive certificate
     end
-	 
-fun read_ct s = read_cterm sg (s, TypeInfer.logicT);
+
+fun read_ct s = read_cterm thy (s, TypeInfer.logicT);
     
 fun is_meta_eq th =
     let
@@ -56,19 +56,19 @@
     
 fun prep ths = (Library.filter is_meta_eq ths) @ (map (standard o mk_meta_eq) (Library.filter (not o is_meta_eq) ths))
 
-fun make ths = Compute.basic_make sg ths
+fun make ths = Compute.basic_make thy ths
 	  
 fun inst_tvar ty thm = 
     let
 	val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
 	val v = TVar (hd (sort ord (term_tvars (prop_of thm))))
     in	
-	standard (Thm.instantiate ([(ctyp_of sg v, ctyp_of sg ty)], []) thm)
+	standard (Thm.instantiate ([(ctyp_of thy v, ctyp_of thy ty)], []) thm)
     end
     
 fun inst_tvars [] thms = thms
   | inst_tvars (ty::tys) thms = inst_tvars tys (map (inst_tvar ty) thms)
-				
+
 val matrix_compute =
     let 
 	val spvecT = FloatSparseMatrixBuilder.real_spvecT
@@ -117,8 +117,8 @@
 	matrix_simplify th
     end
 
-fun realFromStr s = valOf (Real.fromString s)
-fun float2real (x,y) = (realFromStr x) * (Math.pow (2.0, realFromStr y))
+val realFromStr = the o Real.fromString;
+fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y);
 
 end
 
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Presburger.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -992,7 +992,8 @@
 lemma not_true_eq_false: "(~ True) = False" by simp
 
 
-lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)"
+lemma int_eq_number_of_eq:
+  "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
   by simp
 lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)" 
   by (simp only: iszero_number_of_Pls)
@@ -1006,7 +1007,7 @@
 lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)" 
   by simp
 
-lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)"
+lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
   by simp
 
 lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))" 
@@ -1018,18 +1019,20 @@
 lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
   by simp
 
-lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (bin_add y (bin_minus x)))::int))"
+lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
   by simp
-lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (bin_add v w)"
+lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
   by simp
 
-lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (bin_add v (bin_minus w))"
+lemma int_number_of_diff_sym:
+  "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
   by simp
 
-lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (bin_mult v w)"
+lemma int_number_of_mult_sym:
+  "((number_of v)::int) * number_of w = number_of (v * w)"
   by simp
 
-lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (bin_minus v)"
+lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
   by simp
 lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
   by simp
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Real/Float.ML
--- a/src/HOL/Real/Float.ML	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Real/Float.ML	Wed Sep 06 13:48:02 2006 +0200
@@ -7,9 +7,9 @@
 sig
     exception Destruct_floatstr of string
     val destruct_floatstr : (char -> bool) -> (char -> bool) -> string -> bool * string * string * bool * string
-									  
+
     exception Floating_point of string
-				
+
     type floatrep = IntInf.int * IntInf.int
     val approx_dec_by_bin : IntInf.int -> floatrep -> floatrep * floatrep
     val approx_decstr_by_bin : int -> string -> floatrep * floatrep
@@ -351,23 +351,19 @@
 exception Dest_float;
 
 fun mk_intinf ty n =
-    let
-	fun mk_bit n = if n = zero then HOLogic.B0_const else HOLogic.B1_const
-								 
-	fun bin_of n = 
-	    if n = zero then HOLogic.pls_const
-	    else if n = minus_one then HOLogic.min_const
-	    else 
-		let 
-		    (*val (q,r) = IntInf.divMod (n, two): doesn't work in SML 10.0.7, but in newer versions!!!*)
-	            val q = IntInf.div (n, two)
-		    val r = IntInf.mod (n, two)
-		in
-		    HOLogic.bit_const $ bin_of q $ mk_bit r
-		end
-    in 
-	HOLogic.number_of_const ty $ (bin_of n)
-    end
+  let
+    fun mk_bit n = if n = zero then HOLogic.B0_const else HOLogic.B1_const
+    fun bin_of n = 
+      if n = zero then HOLogic.pls_const
+      else if n = minus_one then HOLogic.min_const
+      else let 
+        val (q,r) = IntInf.divMod (n, two)
+      in
+        HOLogic.bit_const $ bin_of q $ mk_bit r
+      end
+  in 
+    HOLogic.number_of_const ty $ (bin_of n)
+  end
 
 fun dest_intinf n = 
     let
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Real/Float.thy
--- a/src/HOL/Real/Float.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Real/Float.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -3,7 +3,9 @@
     Author: Steven Obua
 *)
 
-theory Float imports Real begin
+theory Float
+imports Real
+begin
 
 definition
   pow2 :: "int \<Rightarrow> real"
@@ -177,7 +179,7 @@
   ultimately show ?thesis by auto
 qed
 
-lemma real_is_int_number_of[simp]: "real_is_int ((number_of::bin\<Rightarrow>real) x)"
+lemma real_is_int_number_of[simp]: "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
 proof -
   have neg1: "real_is_int (-1::real)"
   proof -
@@ -187,11 +189,9 @@
   qed
 
   {
-    fix x::int
-    have "!! y. real_is_int ((number_of::bin\<Rightarrow>real) (Abs_Bin x))"
-      apply (simp add: number_of_eq)
-      apply (subst Abs_Bin_inverse)
-      apply (simp add: Bin_def)
+    fix x :: int
+    have "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
+      unfolding number_of_eq
       apply (induct x)
       apply (induct_tac n)
       apply (simp)
@@ -212,13 +212,13 @@
   }
   note Abs_Bin = this
   {
-    fix x :: bin
-    have "? u. x = Abs_Bin u"
-      apply (rule exI[where x = "Rep_Bin x"])
-      apply (simp add: Rep_Bin_inverse)
+    fix x :: int
+    have "? u. x = u"
+      apply (rule exI[where x = "x"])
+      apply (simp)
       done
   }
-  then obtain u::int where "x = Abs_Bin u" by auto
+  then obtain u::int where "x = u" by auto
   with Abs_Bin show ?thesis by auto
 qed
 
@@ -448,17 +448,17 @@
 
 lemma not_true_eq_false: "(~ True) = False" by simp
 
-
 lemmas binarith =
   Pls_0_eq Min_1_eq
-  bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
-  bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
-  bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10
-  bin_add_BIT_11 bin_minus_Pls bin_minus_Min bin_minus_1
-  bin_minus_0 bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0
-  bin_add_Pls_right bin_add_Min_right
+  pred_Pls pred_Min pred_1 pred_0
+  succ_Pls succ_Min succ_1 succ_0
+  add_Pls add_Min add_BIT_0 add_BIT_10
+  add_BIT_11 minus_Pls minus_Min minus_1
+  minus_0 mult_Pls mult_Min mult_num1 mult_num0
+  add_Pls_right add_Min_right
 
-lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)"
+lemma int_eq_number_of_eq:
+  "(((number_of v)::int)=(number_of w)) = iszero ((number_of (v + uminus w))::int)"
   by simp
 
 lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
@@ -473,7 +473,7 @@
 lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)"
   by simp
 
-lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)"
+lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
   by simp
 
 lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
@@ -485,7 +485,7 @@
 lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
   by simp
 
-lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (bin_add y (bin_minus x)))::int))"
+lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
   by simp
 
 lemmas intarithrel =
@@ -494,16 +494,16 @@
   lift_bool[OF int_iszero_number_of_1] int_less_number_of_eq_neg nlift_bool[OF int_not_neg_number_of_Pls] lift_bool[OF int_neg_number_of_Min]
   int_neg_number_of_BIT int_le_number_of_eq
 
-lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (bin_add v w)"
+lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
   by simp
 
-lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (bin_add v (bin_minus w))"
+lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
   by simp
 
-lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (bin_mult v w)"
+lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (v * w)"
   by simp
 
-lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (bin_minus v)"
+lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
   by simp
 
 lemmas intarith = int_number_of_add_sym int_number_of_minus_sym int_number_of_diff_sym int_number_of_mult_sym
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Real/Rational.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -451,7 +451,7 @@
 instance rat :: number ..
 
 defs (overloaded)
-  rat_number_of_def: "(number_of w :: rat) == of_int (Rep_Bin w)"
+  rat_number_of_def: "(number_of w :: rat) == of_int w"
     --{*the type constraint is essential!*}
 
 instance rat :: number_ring
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Real/RealDef.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -922,7 +922,7 @@
 instance real :: number ..
 
 defs (overloaded)
-  real_number_of_def: "(number_of w :: real) == of_int (Rep_Bin w)"
+  real_number_of_def: "(number_of w :: real) == of_int w"
     --{*the type constraint is essential!*}
 
 instance real :: number_ring
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Real/ferrante_rackoff.ML
--- a/src/HOL/Real/ferrante_rackoff.ML	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Real/ferrante_rackoff.ML	Wed Sep 06 13:48:02 2006 +0200
@@ -21,12 +21,12 @@
 val nT = HOLogic.natT;
 val binarith = map thm
   ["Pls_0_eq", "Min_1_eq",
- "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
-  "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
-  "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
-  "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", 
-  "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", 
-  "bin_add_Pls_right", "bin_add_Min_right"];
+ "pred_Pls","pred_Min","pred_1","pred_0",
+  "succ_Pls", "succ_Min", "succ_1", "succ_0",
+  "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10",
+  "add_BIT_11", "minus_Pls", "minus_Min", "minus_1", 
+  "minus_0", "mult_Pls", "mult_Min", "mult_1", "mult_0", 
+  "add_Pls_right", "add_Min_right"];
  val intarithrel = 
      (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
 		"int_le_number_of_eq","int_iszero_number_of_0",
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Wed Sep 06 13:48:02 2006 +0200
@@ -33,12 +33,12 @@
 val presburger_ss = simpset ();
 val binarith = map thm
   ["Pls_0_eq", "Min_1_eq",
- "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
-  "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
-  "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
-  "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", 
-  "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", 
-  "bin_add_Pls_right", "bin_add_Min_right"];
+ "pred_Pls","pred_Min","pred_1","pred_0",
+  "succ_Pls", "succ_Min", "succ_1", "succ_0",
+  "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10",
+  "add_BIT_11", "minus_Pls", "minus_Min", "minus_1", 
+  "minus_0", "mult_Pls", "mult_Min", "mult_num1", "mult_num0", 
+  "add_Pls_right", "add_Min_right"];
  val intarithrel = 
      (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
 		"int_le_number_of_eq","int_iszero_number_of_0",
@@ -116,7 +116,6 @@
 val bT = HOLogic.boolT;
 val bitT = HOLogic.bitT;
 val iT = HOLogic.intT;
-val binT = HOLogic.binT;
 val nT = HOLogic.natT;
 
 (* Allowed Consts in formulae for presburger tactic*)
@@ -162,11 +161,11 @@
 
    ("Numeral.bit.B0", bitT),
    ("Numeral.bit.B1", bitT),
-   ("Numeral.Bit", binT --> bitT --> binT),
-   ("Numeral.Pls", binT),
-   ("Numeral.Min", binT),
-   ("Numeral.number_of", binT --> iT),
-   ("Numeral.number_of", binT --> nT),
+   ("Numeral.Bit", iT --> bitT --> iT),
+   ("Numeral.Pls", iT),
+   ("Numeral.Min", iT),
+   ("Numeral.number_of", iT --> iT),
+   ("Numeral.number_of", iT --> nT),
    ("0", nT),
    ("0", iT),
    ("1", nT),
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/arith_data.ML	Wed Sep 06 13:48:02 2006 +0200
@@ -680,7 +680,7 @@
       end
     (* "?P ((?n::int) mod (number_of ?k)) =
          ((iszero (number_of ?k) --> ?P ?n) &
-          (neg (number_of (bin_minus ?k)) -->
+          (neg (number_of (uminus ?k)) -->
             (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
           (neg (number_of ?k) -->
             (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
@@ -699,8 +699,8 @@
         val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
         val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
                                         (number_of $
-                                          (Const ("Numeral.bin_minus",
-                                            HOLogic.binT --> HOLogic.binT) $ k'))
+                                          (Const ("HOL.uminus",
+                                            HOLogic.intT --> HOLogic.intT) $ k'))
         val zero_leq_j              = Const ("Orderings.less_eq",
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j
         val j_lt_t2                 = Const ("Orderings.less",
@@ -732,7 +732,7 @@
       end
     (* "?P ((?n::int) div (number_of ?k)) =
          ((iszero (number_of ?k) --> ?P 0) &
-          (neg (number_of (bin_minus ?k)) -->
+          (neg (number_of (uminus ?k)) -->
             (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
           (neg (number_of ?k) -->
             (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
@@ -751,8 +751,8 @@
         val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
         val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
                                         (number_of $
-                                          (Const ("Numeral.bin_minus",
-                                            HOLogic.binT --> HOLogic.binT) $ k'))
+                                          (Const ("Numeral.uminus",
+                                            HOLogic.intT --> HOLogic.intT) $ k'))
         val zero_leq_j              = Const ("Orderings.less_eq",
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j
         val j_lt_t2                 = Const ("Orderings.less",
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/ex/Abstract_NAT.thy
--- a/src/HOL/ex/Abstract_NAT.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/ex/Abstract_NAT.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -11,6 +11,8 @@
 
 text {* Axiomatic Natural Numbers (Peano) -- a monomorphic theory. *}
 
+hide (open) const succ
+
 locale NAT =
   fixes zero :: 'n
     and succ :: "'n \<Rightarrow> 'n"
diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/hologic.ML	Wed Sep 06 13:48:02 2006 +0200
@@ -76,7 +76,6 @@
   val bitT: typ
   val B0_const: term
   val B1_const: term
-  val binT: typ
   val pls_const: term
   val min_const: term
   val bit_const: term
@@ -280,26 +279,25 @@
   | dest_nat t = raise TERM ("dest_nat", [t]);
 
 
-(* binary numerals *)
+(* binary numerals and int *)
 
-val binT = Type ("Numeral.bin", []);
-
+val intT = Type ("IntDef.int", []);
 val bitT = Type ("Numeral.bit", []);
 
 val B0_const = Const ("Numeral.bit.B0", bitT);
 val B1_const =  Const ("Numeral.bit.B1", bitT);
 
-val pls_const = Const ("Numeral.Pls", binT)
-and min_const = Const ("Numeral.Min", binT)
-and bit_const = Const ("Numeral.Bit", [binT, bitT] ---> binT);
+val pls_const = Const ("Numeral.Pls", intT)
+and min_const = Const ("Numeral.Min", intT)
+and bit_const = Const ("Numeral.Bit", [intT, bitT] ---> intT);
 
-fun number_of_const T = Const ("Numeral.number_of", binT --> T);
+fun number_of_const T = Const ("Numeral.number_of", intT --> T);
 
 fun int_of [] = 0
   | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs);
 
 (*When called from a print translation, the Numeral qualifier will probably have
-  been removed from Bit, bin.B0, etc.*)
+  been removed from Bit, bit.B0, etc.*)
 fun dest_bit (Const ("Numeral.bit.B0", _)) = 0
   | dest_bit (Const ("Numeral.bit.B1", _)) = 1
   | dest_bit (Const ("bit.B0", _)) = 0
@@ -334,11 +332,6 @@
         in bit_const $ bin_of q $ mk_bit r end;
   in bin_of n end;
 
-
-(* int *)
-
-val intT = Type ("IntDef.int", []);
-
 fun mk_int 0 = Const ("0", intT)
   | mk_int 1 = Const ("1", intT)
   | mk_int i = number_of_const intT $ mk_binum i;
diff -r 3d3d24186352 -r 3078fd2eec7b src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Wed Sep 06 13:48:02 2006 +0200
@@ -609,19 +609,18 @@
 (* parametrized application generators, for instantiation in object logic *)
 (* (axiomatic extensions of extraction kernel *)
 
-fun appgen_rep_bin int_of_numeral thy algbr thmtab strct (app as (c as (_, ty), [bin])) trns =
-  case try (int_of_numeral thy) bin
+fun appgen_rep_bin int_of_numeral thy algbr thmtab strct (app as (c, ts)) trns =
+  case try (int_of_numeral thy) (list_comb (Const c, ts))
    of SOME i => if i < 0 then (*preprocessor eliminates negative numerals*)
         trns
         |> appgen_default thy algbr thmtab (no_strict strct) app
       else
         trns
-        |> exprgen_term thy algbr thmtab (no_strict strct) (Const c)
-        ||>> exprgen_term thy algbr thmtab (no_strict strct) bin
-        |-> (fn (e1, e2) => pair (CodegenThingol.INum (i, e1 `$ e2)))
+        |> appgen_default thy algbr thmtab (no_strict strct) app
+        |-> (fn e => pair (CodegenThingol.INum (i, e)))
     | NONE =>
         trns
-        |> appgen_default thy algbr thmtab strct app;
+        |> appgen_default thy algbr thmtab (no_strict strct) app;
 
 fun appgen_char char_to_index thy algbr thmtab strct (app as ((_, ty), _)) trns =
   case (char_to_index o list_comb o apfst Const) app