--- a/src/CCL/ex/Stream.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/CCL/ex/Stream.thy Sat Jul 21 23:25:00 2007 +0200
@@ -37,7 +37,7 @@
apply (blast intro: 1)
apply safe
apply (drule ListsXH [THEN iffD1])
- apply (tactic "EQgen_tac (simpset ()) [] 1")
+ apply (tactic "EQgen_tac @{context} [] 1")
apply fastsimp
done
@@ -51,7 +51,7 @@
apply (blast intro: 1)
apply safe
apply (drule ListsXH [THEN iffD1])
- apply (tactic "EQgen_tac (simpset ()) [] 1")
+ apply (tactic "EQgen_tac @{context} [] 1")
apply blast
done
@@ -67,9 +67,9 @@
apply (blast intro: prems)
apply safe
apply (drule ListsXH [THEN iffD1])
- apply (tactic "EQgen_tac (simpset ()) [] 1")
+ apply (tactic "EQgen_tac @{context} [] 1")
apply (drule ListsXH [THEN iffD1])
- apply (tactic "EQgen_tac (simpset ()) [] 1")
+ apply (tactic "EQgen_tac @{context} [] 1")
apply blast
done
@@ -86,11 +86,11 @@
apply (blast intro: prems)
apply safe
apply (drule ListsXH [THEN iffD1])
- apply (tactic "EQgen_tac (simpset ()) [] 1")
+ apply (tactic "EQgen_tac @{context} [] 1")
prefer 2
apply blast
apply (tactic {* DEPTH_SOLVE (etac (XH_to_E (thm "ListsXH")) 1
- THEN EQgen_tac (simpset ()) [] 1) *})
+ THEN EQgen_tac @{context} [] 1) *})
done
@@ -104,7 +104,7 @@
apply (blast intro: prems)
apply safe
apply (drule IListsXH [THEN iffD1])
- apply (tactic "EQgen_tac (simpset ()) [] 1")
+ apply (tactic "EQgen_tac @{context} [] 1")
apply blast
done
@@ -136,7 +136,7 @@
apply (tactic {* eq_coinduct3_tac
"{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 (simpset ()) [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