src/ZF/Bin.thy

 consts  bin :: i
 datatype
   "bin" = Pls
         | Min
         | Bit ("w: bin", "b: bool")     (infixl "BIT" 90)
-
-use "Tools/numeral_syntax.ML"
-
-syntax
-  "_Int"    :: "xnum => i"        ("_")
 
 consts
   integ_of  :: "i=>i"
   NCons     :: "[i,i]=>i"
   bin_succ  :: "i=>i"

     "bin_mult (Min,w)     = bin_minus(w)"
   bin_mult_BIT:
     "bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
                                  NCons(bin_mult(v,w),0))"
 
+syntax
+  "_Int"    :: "xnum => i"        ("_")
+
+use "Tools/numeral_syntax.ML"
 setup NumeralSyntax.setup
 
 
 declare bin.intros [simp,TC]