src/ZF/Integ/Bin.thy
changeset 6117 f9aad8ccd590
parent 6046 2c8a8be36c94
child 6153 bff90585cce5
     1.1 --- a/src/ZF/Integ/Bin.thy	Wed Jan 13 12:44:33 1999 +0100
     1.2 +++ b/src/ZF/Integ/Bin.thy	Wed Jan 13 15:14:47 1999 +0100
     1.3 @@ -20,6 +20,15 @@
     1.4  
     1.5  Bin = Int + Datatype + 
     1.6  
     1.7 +consts  bin :: i
     1.8 +datatype
     1.9 +  "bin" = Pls
    1.10 +        | Min
    1.11 +        | Cons ("w: bin", "b: bool")
    1.12 +
    1.13 +syntax
    1.14 +  "_Int"           :: xnum => i        ("_")
    1.15 +
    1.16  consts
    1.17    integ_of  :: i=>i
    1.18    NCons     :: [i,i]=>i
    1.19 @@ -30,18 +39,6 @@
    1.20    adding    :: [i,i,i]=>i
    1.21    bin_mult  :: [i,i]=>i
    1.22  
    1.23 -  bin       :: i
    1.24 -
    1.25 -syntax
    1.26 -  "_Int"           :: xnum => i        ("_")
    1.27 -
    1.28 -datatype
    1.29 -  "bin" = Pls
    1.30 -        | Min
    1.31 -        | Cons ("w: bin", "b: bool")
    1.32 -  type_intrs "[bool_into_univ]"
    1.33 -
    1.34 -
    1.35  primrec
    1.36    "integ_of (Pls)       = $# 0"
    1.37    "integ_of (Min)       = $~($#1)"