# HG changeset patch
# User kleing
# Date 1016975153 -3600
# Node ID d6585b32412bab4ee97602671d1578d3dc93fc57
# Parent  1f54a5fecaa67396f2e8b5dff53353a10590dd69
more about match_exception_table

diff -r 1f54a5fecaa6 -r d6585b32412b src/HOL/MicroJava/JVM/JVMExceptions.thy
--- 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