# HG changeset patch
# User lcp
# Date 787595983 -3600
# Node ID 13aa1e3d8a3a1b77857a5dee22f8d3026a27c214
# Parent  31ec33d9623129df79a503c1e0ed897ff75c3d77
put quotation marks around constant "and" because it is a
keyword for inductive definitions!!

diff -r 31ec33d96231 -r 13aa1e3d8a3a src/ZF/Bool.thy
--- 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)