--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy Thu Mar 21 16:40:18 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy Sun Mar 24 14:05:53 2002 +0100
@@ -87,4 +87,14 @@
apply (auto simp add: blank_def)
done
+
+text {*
+ Only program counters that are mentioned in the exception table
+ can be returned by @{term match_exception_table}:
+*}
+lemma match_exception_table_in_et:
+ "match_exception_table G C pc et = Some pc' \<Longrightarrow> \<exists>e \<in> set et. pc' = fst (snd (snd e))"
+ by (induct et) (auto split: split_if_asm)
+
+
end