src/ZF/Bool.ML

 For ZF/bool.thy.  Booleans in Zermelo-Fraenkel Set Theory 
 *)
 
 open Bool;
 
-val bool_defs = [bool_def,one_def,cond_def];
+val bool_defs = [bool_def,cond_def];
 
 (* Introduction rules *)
 
 goalw Bool.thy bool_defs "1 : bool";
 by (rtac (consI1 RS consI2) 1);