put quotation marks around constant "and" because it is a
keyword for inductive definitions!!
--- a/src/ZF/Bool.thy Fri Dec 16 17:38:14 1994 +0100
+++ b/src/ZF/Bool.thy Fri Dec 16 17:39:43 1994 +0100
@@ -12,7 +12,7 @@
bool :: "i"
cond :: "[i,i,i]=>i"
not :: "i=>i"
- and :: "[i,i]=>i" (infixl 70)
+ "and" :: "[i,i]=>i" (infixl 70)
or :: "[i,i]=>i" (infixl 65)
xor :: "[i,i]=>i" (infixl 65)