--- a/src/CCL/ex/Stream.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/CCL/ex/Stream.thy Mon Sep 06 19:13:10 2010 +0200
@@ -88,7 +88,7 @@
apply (tactic "EQgen_tac @{context} [] 1")
prefer 2
apply blast
- apply (tactic {* DEPTH_SOLVE (etac (XH_to_E (thm "ListsXH")) 1
+ apply (tactic {* DEPTH_SOLVE (etac (XH_to_E @{thm ListsXH}) 1
THEN EQgen_tac @{context} [] 1) *})
done
@@ -135,7 +135,7 @@
apply (tactic {* eq_coinduct3_tac @{context}
"{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*})
apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong])
- apply (tactic {* EQgen_tac @{context} [thm "iter1B", thm "iter2Blemma"] 1 *})
+ apply (tactic {* EQgen_tac @{context} [@{thm iter1B}, @{thm iter2Blemma}] 1 *})
apply (subst napply_f, assumption)
apply (rule_tac f1 = f in napplyBsucc [THEN subst])
apply blast