# HG changeset patch
# User kleing
# Date 1015702759 -3600
# Node ID 8efb5d92cf552288752f10fb59928e03f86a79b6
# Parent  04deb0c8dcbe73ac70fa33cc3443e331b0bdea81
in wellformed programs, exceptions are classes

diff -r 04deb0c8dcbe -r 8efb5d92cf55 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Fri Mar 08 20:39:39 2002 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Sat Mar 09 20:39:19 2002 +0100
@@ -70,6 +70,15 @@
 apply (simp (no_asm_simp))
 done
 
+lemma is_class_xcpt [simp]: "wf_prog wf_mb G \<Longrightarrow> is_class G (Xcpt x)"
+  apply (simp add: wf_prog_def wf_syscls_def)
+  apply (simp add: is_class_def class_def)
+  apply clarify
+  apply (erule_tac x = x in allE)
+  apply clarify
+  apply (auto intro!: map_of_SomeI)
+  done
+
 lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; wf_prog wf_mb G|] ==> D \<noteq> C \<and> \<not>(D,C)\<in>(subcls1 G)^+"
 apply( frule r_into_trancl)
 apply( drule subcls1D)