--- a/src/HOL/MicroJava/BV/BVExample.thy Mon May 26 11:42:41 2003 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Mon May 26 18:36:15 2003 +0200
@@ -186,6 +186,7 @@
text {*
The program is structurally wellformed:
*}
+
lemma wf_struct:
"wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")
proof -
@@ -223,7 +224,8 @@
apply (auto simp add: name_defs distinct_classes distinct_fields)
done
ultimately
- show ?thesis by (simp add: wf_prog_def E_def SystemClasses_def)
+ show ?thesis
+ by (simp add: wf_prog_def ws_prog_def wf_cdecl_mrT_cdecl_mdecl E_def SystemClasses_def)
qed
section "Welltypings"