--- a/src/CTT/Bool.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/CTT/Bool.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CTT/bool
+(* Title: CTT/bool
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
The two-element type (booleans and conditionals)
@@ -8,12 +8,12 @@
Bool = CTT +
-consts Bool :: "t"
- true,false :: "i"
- cond :: "[i,i,i]=>i"
+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)"
+ 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