diff -r 8efb5d92cf55 -r 3bf41c474a88 src/HOL/MicroJava/JVM/JVMState.thy
--- a/src/HOL/MicroJava/JVM/JVMState.thy	Sat Mar 09 20:39:19 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMState.thy	Sat Mar 09 20:39:46 2002 +0100
@@ -46,6 +46,16 @@
   jvm_state = "val option \<times> aheap \<times> frame list"  -- "exception flag, heap, frames"
 
 
+text {* a new, blank object with default values in all fields: *}
+constdefs
+  blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj"
+  "blank G C \<equiv> (C,init_vars (fields(G,C)))" 
+
+  start_heap :: "'c prog \<Rightarrow> aheap"
+  "start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer))
+                      (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast))
+                      (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"
+
 section {* Lemmas *}
 
 lemma new_AddrD:
@@ -68,6 +78,6 @@
   assume "snd (new_Addr hp) = Some xcp" 
   ultimately
   show ?thesis by (auto dest: new_AddrD)
-qed  
-
+qed
+  
 end
\ No newline at end of file