equal
deleted
inserted
replaced
206 |
206 |
207 lemma xcpt_names_in_et: |
207 lemma xcpt_names_in_et: |
208 "C \<in> set (xcpt_names (i,G,pc,et)) \<Longrightarrow> |
208 "C \<in> set (xcpt_names (i,G,pc,et)) \<Longrightarrow> |
209 \<exists>e \<in> set et. the (match_exception_table G C pc et) = fst (snd (snd e))" |
209 \<exists>e \<in> set et. the (match_exception_table G C pc et) = fst (snd (snd e))" |
210 apply (cases i) |
210 apply (cases i) |
211 apply (auto iff: not_None_eq |
211 apply (auto dest!: match_any_match_table match_X_match_table |
212 dest!: match_any_match_table match_X_match_table |
|
213 dest: match_exception_table_in_et) |
212 dest: match_exception_table_in_et) |
214 done |
213 done |
215 |
214 |
216 |
215 |
217 lemma 1: "2 < length a \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)" |
216 lemma 1: "2 < length a \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)" |