src/ZF/bool.thy

--- a/src/ZF/bool.thy	Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/bool.thy	Thu Sep 30 10:10:21 1993 +0100
@@ -16,8 +16,10 @@
     or		::      "[i,i]=>i"      (infixl 65)
     xor		::      "[i,i]=>i"      (infixl 65)
 
+translations
+   "1"  == "succ(0)"
+
 rules
-    one_def 	"1    == succ(0)"
     bool_def	"bool == {0,1}"
     cond_def	"cond(b,c,d) == if(b=1,c,d)"
     not_def	"not(b) == cond(b,0,1)"