| changeset 44890 | 22f665a2e91c |
| parent 42151 | 4da4fc77664b |
| child 47026 | 36dacca8a95c |
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Sun Sep 11 22:56:05 2011 +0200 +++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Mon Sep 12 07:55:43 2011 +0200 @@ -197,9 +197,9 @@ apply (tactic {* pair_tac @{context} "a" 1 *}) apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *}) apply blast -apply fastsimp +apply fastforce apply (tactic {* pair_tac @{context} "a" 1 *}) - apply fastsimp + apply fastforce done end