src/CCL/ex/Nat.thy
changeset 27221 31328dc30196
parent 24825 c4f13ab78f9d
child 35762 af3ff2ba4c54
     1.1 --- a/src/CCL/ex/Nat.thy	Sat Jun 14 23:33:43 2008 +0200
     1.2 +++ b/src/CCL/ex/Nat.thy	Sat Jun 14 23:52:51 2008 +0200
     1.3 @@ -61,32 +61,32 @@
     1.4  
     1.5  lemma addT: "[| a:Nat;  b:Nat |] ==> a #+ b : Nat"
     1.6    apply (unfold add_def)
     1.7 -  apply (tactic {* typechk_tac [] 1 *})
     1.8 +  apply (tactic {* typechk_tac @{context} [] 1 *})
     1.9    done
    1.10  
    1.11  lemma multT: "[| a:Nat;  b:Nat |] ==> a #* b : Nat"
    1.12    apply (unfold add_def mult_def)
    1.13 -  apply (tactic {* typechk_tac [] 1 *})
    1.14 +  apply (tactic {* typechk_tac @{context} [] 1 *})
    1.15    done
    1.16  
    1.17  (* Defined to return zero if a<b *)
    1.18  lemma subT: "[| a:Nat;  b:Nat |] ==> a #- b : Nat"
    1.19    apply (unfold sub_def)
    1.20 -  apply (tactic {* typechk_tac [] 1 *})
    1.21 -  apply (tactic clean_ccs_tac)
    1.22 +  apply (tactic {* typechk_tac @{context} [] 1 *})
    1.23 +  apply (tactic {* clean_ccs_tac @{context} *})
    1.24    apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
    1.25    done
    1.26  
    1.27  lemma leT: "[| a:Nat;  b:Nat |] ==> a #<= b : Bool"
    1.28    apply (unfold le_def)
    1.29 -  apply (tactic {* typechk_tac [] 1 *})
    1.30 -  apply (tactic clean_ccs_tac)
    1.31 +  apply (tactic {* typechk_tac @{context} [] 1 *})
    1.32 +  apply (tactic {* clean_ccs_tac @{context} *})
    1.33    apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
    1.34    done
    1.35  
    1.36  lemma ltT: "[| a:Nat;  b:Nat |] ==> a #< b : Bool"
    1.37    apply (unfold not_def lt_def)
    1.38 -  apply (tactic {* typechk_tac [thm "leT"] 1 *})
    1.39 +  apply (tactic {* typechk_tac @{context} @{thms leT} 1 *})
    1.40    done
    1.41  
    1.42  
    1.43 @@ -96,9 +96,8 @@
    1.44  
    1.45  lemma "[| a:Nat;  b:Nat |] ==> ackermann(a,b) : Nat"
    1.46    apply (unfold ack_def)
    1.47 -  apply (tactic "gen_ccs_tac [] 1")
    1.48 +  apply (tactic {* gen_ccs_tac @{context} [] 1 *})
    1.49    apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+
    1.50    done
    1.51  
    1.52  end
    1.53 -