src/ZF/Bool.thy
changeset 1401 0c439768f45c
parent 837 778f01546669
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/Bool.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/Bool.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -10,14 +10,14 @@
     1.4  
     1.5  Bool = ZF + "simpdata" +
     1.6  consts
     1.7 -    "1"		:: "i"     	   ("1")
     1.8 -    "2"         :: "i"             ("2")
     1.9 -    bool        :: "i"
    1.10 -    cond        :: "[i,i,i]=>i"
    1.11 -    not		:: "i=>i"
    1.12 -    "and"       :: "[i,i]=>i"      (infixl 70)
    1.13 -    or		:: "[i,i]=>i"      (infixl 65)
    1.14 -    xor		:: "[i,i]=>i"      (infixl 65)
    1.15 +    "1"		:: i     	   ("1")
    1.16 +    "2"         :: i             ("2")
    1.17 +    bool        :: i
    1.18 +    cond        :: [i,i,i]=>i
    1.19 +    not		:: i=>i
    1.20 +    "and"       :: [i,i]=>i      (infixl 70)
    1.21 +    or		:: [i,i]=>i      (infixl 65)
    1.22 +    xor		:: [i,i]=>i      (infixl 65)
    1.23  
    1.24  translations
    1.25     "1"  == "succ(0)"