equal
deleted
inserted
replaced
50 Only program counters that are mentioned in the exception table |
50 Only program counters that are mentioned in the exception table |
51 can be returned by @{term match_exception_table}: |
51 can be returned by @{term match_exception_table}: |
52 \<close> |
52 \<close> |
53 lemma match_exception_table_in_et: |
53 lemma match_exception_table_in_et: |
54 "match_exception_table G C pc et = Some pc' \<Longrightarrow> \<exists>e \<in> set et. pc' = fst (snd (snd e))" |
54 "match_exception_table G C pc et = Some pc' \<Longrightarrow> \<exists>e \<in> set et. pc' = fst (snd (snd e))" |
55 by (induct et) (auto split: split_if_asm) |
55 by (induct et) (auto split: if_split_asm) |
56 |
56 |
57 |
57 |
58 end |
58 end |