src/CTT/Bool.thy
changeset 3837 d7f033c74b38
parent 1474 3f7d67927fe2
child 17441 5b5feca0344a
--- a/src/CTT/Bool.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/Bool.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -15,5 +15,5 @@
   Bool_def      "Bool == T+T"
   true_def      "true == inl(tt)"
   false_def     "false == inr(tt)"
-  cond_def      "cond(a,b,c) == when(a, %u.b, %u.c)"
+  cond_def      "cond(a,b,c) == when(a, %u. b, %u. c)"
 end