| changeset 27208 | 5fe899199f85 |
| parent 25131 | 2c8caac48ade |
| child 28524 | 644b62cf678f |
--- a/src/HOLCF/IOA/meta_theory/TL.thy Sat Jun 14 17:49:24 2008 +0200 +++ b/src/HOLCF/IOA/meta_theory/TL.thy Sat Jun 14 23:19:51 2008 +0200 @@ -155,7 +155,7 @@ "s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s" apply (unfold tsuffix_def suffix_def) apply auto -apply (tactic {* Seq_case_simp_tac "s" 1 *}) +apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *}) apply (rule_tac x = "a>>s1" in exI) apply auto done