src/CTT/Bool.thy

--- a/src/CTT/Bool.thy	Tue Nov 11 10:54:52 2014 +0100
+++ b/src/CTT/Bool.thy	Tue Nov 11 11:41:58 2014 +0100
@@ -33,7 +33,7 @@
 (*formation rule*)
 lemma boolF: "Bool type"
 apply (unfold bool_defs)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
 done
 
 
@@ -41,21 +41,21 @@
 
 lemma boolI_true: "true : Bool"
 apply (unfold bool_defs)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
 done
 
 lemma boolI_false: "false : Bool"
 apply (unfold bool_defs)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
 done
 
 (*elimination rule: typing of cond*)
 lemma boolE: 
     "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
 apply (unfold bool_defs)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
 apply (erule_tac [!] TE)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
 done
 
 lemma boolEL: 
@@ -72,18 +72,18 @@
     "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
 apply (unfold bool_defs)
 apply (rule comp_rls)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
 apply (erule_tac [!] TE)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
 done
 
 lemma boolC_false: 
     "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
 apply (unfold bool_defs)
 apply (rule comp_rls)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
 apply (erule_tac [!] TE)
-apply (tactic "typechk_tac @{context} []")
+apply typechk
 done
 
 end