Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more antiquotations;
authorwenzelm
Tue, 25 Mar 2008 19:39:57 +0100
changeset 26391 6e8aa5a4eb82
parent 26390 99d4cbb1f941
child 26392 748b263f0e40
more antiquotations;
src/CCL/Wfd.thy file | annotate | diff | comparison | revisions
src/CTT/CTT.thy file | annotate | diff | comparison | revisions 
--- a/src/CCL/Wfd.thy	Tue Mar 25 12:14:17 2008 +0100
+++ b/src/CCL/Wfd.thy	Tue Mar 25 19:39:57 2008 +0100
@@ -539,8 +539,8 @@
   apply (unfold let_def)
   apply (rule 1 [THEN canonical])
   apply (tactic {*
-    REPEAT (DEPTH_SOLVE_1 (resolve_tac (thms "prems" @ thms "eval_rls") 1 ORELSE
-                           etac (thm "substitute") 1)) *})
+    REPEAT (DEPTH_SOLVE_1 (resolve_tac (@{thms assms} @ @{thms eval_rls}) 1 ORELSE
+      etac @{thm substitute} 1)) *})
   done
 
 lemma fixV: "f(fix(f)) ---> c ==> fix(f) ---> c"
--- a/src/CTT/CTT.thy	Tue Mar 25 12:14:17 2008 +0100
+++ b/src/CTT/CTT.thy	Tue Mar 25 19:39:57 2008 +0100
@@ -500,7 +500,7 @@
   apply (unfold basic_defs)
   apply (rule major [THEN SumE])
   apply (rule SumC [THEN subst_eqtyparg, THEN replace_type])
-  apply (tactic {* typechk_tac (thms "prems") *})
+  apply (tactic {* typechk_tac @{thms assms} *})
   done
 
 end
isabelle