equal
deleted
inserted
replaced
113 show ?thesis by auto |
113 show ?thesis by auto |
114 qed |
114 qed |
115 qed |
115 qed |
116 |
116 |
117 lemma match_et_imp_match: |
117 lemma match_et_imp_match: |
118 "match_exception_table G X pc et = Some handler |
118 "match_exception_table G (Xcpt X) pc et = Some handler |
119 \<Longrightarrow> match G X pc et = [X]" |
119 \<Longrightarrow> match G X pc et = [Xcpt X]" |
120 apply (simp add: match_some_entry) |
120 apply (simp add: match_some_entry) |
121 apply (induct et) |
121 apply (induct et) |
122 apply (auto split: split_if_asm) |
122 apply (auto split: split_if_asm) |
123 done |
123 done |
124 |
124 |