| changeset 56073 | 29e308b56d23 |
| parent 51703 | f2e92fc0c8aa |
| child 58880 | 0baae4311a9f |
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Wed Mar 12 22:57:50 2014 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Thu Mar 13 07:07:07 2014 +0100 @@ -196,10 +196,7 @@ apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *}) apply (tactic {* pair_tac @{context} "a" 1 *}) apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *}) -apply blast -apply fastforce apply (tactic {* pair_tac @{context} "a" 1 *}) - apply fastforce done end