--- a/src/ZF/Integ/Bin.thy Wed Jan 13 12:44:33 1999 +0100
+++ b/src/ZF/Integ/Bin.thy Wed Jan 13 15:14:47 1999 +0100
@@ -20,6 +20,15 @@
Bin = Int + Datatype +
+consts bin :: i
+datatype
+ "bin" = Pls
+ | Min
+ | Cons ("w: bin", "b: bool")
+
+syntax
+ "_Int" :: xnum => i ("_")
+
consts
integ_of :: i=>i
NCons :: [i,i]=>i
@@ -30,18 +39,6 @@
adding :: [i,i,i]=>i
bin_mult :: [i,i]=>i
- bin :: i
-
-syntax
- "_Int" :: xnum => i ("_")
-
-datatype
- "bin" = Pls
- | Min
- | Cons ("w: bin", "b: bool")
- type_intrs "[bool_into_univ]"
-
-
primrec
"integ_of (Pls) = $# 0"
"integ_of (Min) = $~($#1)"