src/CCL/ex/Nat.thy

--- a/src/CCL/ex/Nat.thy	Sat Jun 14 23:33:43 2008 +0200
+++ b/src/CCL/ex/Nat.thy	Sat Jun 14 23:52:51 2008 +0200
@@ -61,32 +61,32 @@
 
 lemma addT: "[| a:Nat;  b:Nat |] ==> a #+ b : Nat"
   apply (unfold add_def)
-  apply (tactic {* typechk_tac [] 1 *})
+  apply (tactic {* typechk_tac @{context} [] 1 *})
   done
 
 lemma multT: "[| a:Nat;  b:Nat |] ==> a #* b : Nat"
   apply (unfold add_def mult_def)
-  apply (tactic {* typechk_tac [] 1 *})
+  apply (tactic {* typechk_tac @{context} [] 1 *})
   done
 
 (* Defined to return zero if a<b *)
 lemma subT: "[| a:Nat;  b:Nat |] ==> a #- b : Nat"
   apply (unfold sub_def)
-  apply (tactic {* typechk_tac [] 1 *})
-  apply (tactic clean_ccs_tac)
+  apply (tactic {* typechk_tac @{context} [] 1 *})
+  apply (tactic {* clean_ccs_tac @{context} *})
   apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
   done
 
 lemma leT: "[| a:Nat;  b:Nat |] ==> a #<= b : Bool"
   apply (unfold le_def)
-  apply (tactic {* typechk_tac [] 1 *})
-  apply (tactic clean_ccs_tac)
+  apply (tactic {* typechk_tac @{context} [] 1 *})
+  apply (tactic {* clean_ccs_tac @{context} *})
   apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
   done
 
 lemma ltT: "[| a:Nat;  b:Nat |] ==> a #< b : Bool"
   apply (unfold not_def lt_def)
-  apply (tactic {* typechk_tac [thm "leT"] 1 *})
+  apply (tactic {* typechk_tac @{context} @{thms leT} 1 *})
   done
 
 
@@ -96,9 +96,8 @@
 
 lemma "[| a:Nat;  b:Nat |] ==> ackermann(a,b) : Nat"
   apply (unfold ack_def)
-  apply (tactic "gen_ccs_tac [] 1")
+  apply (tactic {* gen_ccs_tac @{context} [] 1 *})
   apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+
   done
 
 end
-