diff -r 000000000000 -r a5a9c433f639 src/CTT/bool.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CTT/bool.thy	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,19 @@
+(*  Title: 	CTT/bool
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1991  University of Cambridge
+
+The two-element type (booleans and conditionals)
+*)
+
+Bool = CTT +
+
+consts Bool		:: "t"
+       true,false	:: "i"
+       cond		:: "[i,i,i]=>i"
+rules
+  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)"
+end