--- a/src/CCL/ex/Stream.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/CCL/ex/Stream.thy Sat Jun 14 23:19:51 2008 +0200
@@ -32,7 +32,7 @@
lemma map_comp:
assumes 1: "l:Lists(A)"
shows "map(f o g,l) = map(f,map(g,l))"
- apply (tactic {* eq_coinduct3_tac
+ apply (tactic {* eq_coinduct3_tac @{context}
"{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (f o g,l) & y=map (f,map (g,l)))}" 1 *})
apply (blast intro: 1)
apply safe
@@ -46,7 +46,7 @@
lemma map_id:
assumes 1: "l:Lists(A)"
shows "map(%x. x,l) = l"
- apply (tactic {* eq_coinduct3_tac
+ apply (tactic {* eq_coinduct3_tac @{context}
"{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (%x. x,l) & y=l) }" 1 *})
apply (blast intro: 1)
apply safe
@@ -62,7 +62,7 @@
assumes "l:Lists(A)"
and "m:Lists(A)"
shows "map(f,l@m) = map(f,l) @ map(f,m)"
- apply (tactic {* eq_coinduct3_tac
+ apply (tactic {* eq_coinduct3_tac @{context}
"{p. EX x y. p=<x,y> & (EX l:Lists (A). EX m:Lists (A). x=map (f,l@m) & y=map (f,l) @ map (f,m))}" 1 *})
apply (blast intro: prems)
apply safe
@@ -81,7 +81,7 @@
and "l:Lists(A)"
and "m:Lists(A)"
shows "k @ l @ m = (k @ l) @ m"
- apply (tactic {* eq_coinduct3_tac
+ apply (tactic {* eq_coinduct3_tac @{context}
"{p. EX x y. p=<x,y> & (EX k:Lists (A). EX l:Lists (A). EX m:Lists (A). x=k @ l @ m & y= (k @ l) @ m) }" 1*})
apply (blast intro: prems)
apply safe
@@ -99,7 +99,7 @@
lemma ilist_append:
assumes "l:ILists(A)"
shows "l @ m = l"
- apply (tactic {* eq_coinduct3_tac
+ apply (tactic {* eq_coinduct3_tac @{context}
"{p. EX x y. p=<x,y> & (EX l:ILists (A) .EX m. x=l@m & y=l)}" 1 *})
apply (blast intro: prems)
apply safe
@@ -133,7 +133,7 @@
done
lemma iter1_iter2_eq: "iter1(f,a) = iter2(f,a)"
- apply (tactic {* eq_coinduct3_tac
+ 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 *})