src/ZF/Bool.thy
changeset 753 ec86863e87c8
parent 124 858ab9a9b047
child 799 13aa1e3d8a3a
     1.1 --- a/src/ZF/Bool.thy	Mon Nov 28 19:48:30 1994 +0100
     1.2 +++ b/src/ZF/Bool.thy	Tue Nov 29 00:31:31 1994 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  translations
     1.5     "1"  == "succ(0)"
     1.6  
     1.7 -rules
     1.8 +defs
     1.9      bool_def	"bool == {0,1}"
    1.10      cond_def	"cond(b,c,d) == if(b=1,c,d)"
    1.11      not_def	"not(b) == cond(b,0,1)"