src/ZF/Bool.thy
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)"