equal
deleted
inserted
replaced
146 lemma tsuffix_TL [rule_format (no_asm)]: |
146 lemma tsuffix_TL [rule_format (no_asm)]: |
147 "s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s" |
147 "s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s" |
148 apply (unfold tsuffix_def suffix_def) |
148 apply (unfold tsuffix_def suffix_def) |
149 apply auto |
149 apply auto |
150 apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *}) |
150 apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *}) |
151 apply (rule_tac x = "a>>s1" in exI) |
151 apply (rule_tac x = "a\<leadsto>s1" in exI) |
152 apply auto |
152 apply auto |
153 done |
153 done |
154 |
154 |
155 lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL] |
155 lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL] |
156 |
156 |