src/CTT/Bool.thy

--- a/src/CTT/Bool.thy	Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CTT/Bool.thy	Tue Nov 11 15:55:31 2014 +0100
@@ -22,8 +22,8 @@
   "false == inr(tt)"
 
 definition
-  cond :: "[i,i,i]=>i" where
-  "cond(a,b,c) == when(a, %u. b, %u. c)"
+  cond :: "[i,i,i]\<Rightarrow>i" where
+  "cond(a,b,c) == when(a, \<lambda>u. b, \<lambda>u. c)"
 
 lemmas bool_defs = Bool_def true_def false_def cond_def
 
@@ -50,17 +50,15 @@
 done
 
 (*elimination rule: typing of cond*)
-lemma boolE: 
-    "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
+lemma boolE: "\<lbrakk>p:Bool; a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(p,a,b) : C(p)"
 apply (unfold bool_defs)
 apply typechk
 apply (erule_tac [!] TE)
 apply typechk
 done
 
-lemma boolEL: 
-    "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |]  
-     ==> cond(p,a,b) = cond(q,c,d) : C(p)"
+lemma boolEL: "\<lbrakk>p = q : Bool; a = c : C(true); b = d : C(false)\<rbrakk>
+  \<Longrightarrow> cond(p,a,b) = cond(q,c,d) : C(p)"
 apply (unfold bool_defs)
 apply (rule PlusEL)
 apply (erule asm_rl refl_elem [THEN TEL])+
@@ -68,8 +66,7 @@
 
 (*computation rules for true, false*)
 
-lemma boolC_true: 
-    "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
+lemma boolC_true: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(true,a,b) = a : C(true)"
 apply (unfold bool_defs)
 apply (rule comp_rls)
 apply typechk
@@ -77,8 +74,7 @@
 apply typechk
 done
 
-lemma boolC_false: 
-    "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
+lemma boolC_false: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(false,a,b) = b : C(false)"
 apply (unfold bool_defs)
 apply (rule comp_rls)
 apply typechk