changeset 60754 | 02924903a6fd |
parent 59807 | 22bc39064290 |
child 60770 | 240563fbf41d |
--- a/src/CCL/ex/Stream.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/CCL/ex/Stream.thy Sat Jul 18 20:54:56 2015 +0200 @@ -82,7 +82,7 @@ apply EQgen prefer 2 apply blast - apply (tactic {* DEPTH_SOLVE (etac (XH_to_E @{thm ListsXH}) 1 + apply (tactic {* DEPTH_SOLVE (eresolve_tac @{context} [XH_to_E @{thm ListsXH}] 1 THEN EQgen_tac @{context} [] 1) *}) done