src/ZF/Bool.thy
changeset 14 1c0926788772
parent 0 a5a9c433f639
child 124 858ab9a9b047
     1.1 --- a/src/ZF/Bool.thy	Fri Sep 24 11:27:15 1993 +0200
     1.2 +++ b/src/ZF/Bool.thy	Thu Sep 30 10:10:21 1993 +0100
     1.3 @@ -16,8 +16,10 @@
     1.4      or		::      "[i,i]=>i"      (infixl 65)
     1.5      xor		::      "[i,i]=>i"      (infixl 65)
     1.6  
     1.7 +translations
     1.8 +   "1"  == "succ(0)"
     1.9 +
    1.10  rules
    1.11 -    one_def 	"1    == succ(0)"
    1.12      bool_def	"bool == {0,1}"
    1.13      cond_def	"cond(b,c,d) == if(b=1,c,d)"
    1.14      not_def	"not(b) == cond(b,0,1)"