| changeset 2539 | ddd22ceee8cc | 
| parent 2469 | b50b8c0eec01 | 
| child 9570 | e16e168984e1 | 
--- a/src/ZF/Bool.thy Thu Jan 23 10:35:28 1997 +0100 +++ b/src/ZF/Bool.thy Thu Jan 23 10:40:21 1997 +0100 @@ -10,8 +10,6 @@ Bool = upair + consts - "1" :: i ("1") - "2" :: i ("2") bool :: i cond :: [i,i,i]=>i not :: i=>i @@ -19,6 +17,10 @@ or :: [i,i]=>i (infixl 65) xor :: [i,i]=>i (infixl 65) +syntax + "1" :: i ("1") + "2" :: i ("2") + translations "1" == "succ(0)" "2" == "succ(1)"