more antiquotations;
authorwenzelm
Tue Mar 25 19:39:57 2008 +0100 (2008-03-25)
changeset 263916e8aa5a4eb82
parent 26390 99d4cbb1f941
child 26392 748b263f0e40
more antiquotations;
src/CCL/Wfd.thy
src/CTT/CTT.thy
     1.1 --- a/src/CCL/Wfd.thy	Tue Mar 25 12:14:17 2008 +0100
     1.2 +++ b/src/CCL/Wfd.thy	Tue Mar 25 19:39:57 2008 +0100
     1.3 @@ -539,8 +539,8 @@
     1.4    apply (unfold let_def)
     1.5    apply (rule 1 [THEN canonical])
     1.6    apply (tactic {*
     1.7 -    REPEAT (DEPTH_SOLVE_1 (resolve_tac (thms "prems" @ thms "eval_rls") 1 ORELSE
     1.8 -                           etac (thm "substitute") 1)) *})
     1.9 +    REPEAT (DEPTH_SOLVE_1 (resolve_tac (@{thms assms} @ @{thms eval_rls}) 1 ORELSE
    1.10 +      etac @{thm substitute} 1)) *})
    1.11    done
    1.12  
    1.13  lemma fixV: "f(fix(f)) ---> c ==> fix(f) ---> c"
     2.1 --- a/src/CTT/CTT.thy	Tue Mar 25 12:14:17 2008 +0100
     2.2 +++ b/src/CTT/CTT.thy	Tue Mar 25 19:39:57 2008 +0100
     2.3 @@ -500,7 +500,7 @@
     2.4    apply (unfold basic_defs)
     2.5    apply (rule major [THEN SumE])
     2.6    apply (rule SumC [THEN subst_eqtyparg, THEN replace_type])
     2.7 -  apply (tactic {* typechk_tac (thms "prems") *})
     2.8 +  apply (tactic {* typechk_tac @{thms assms} *})
     2.9    done
    2.10  
    2.11  end