diff -r eec2582923f6 -r b95d12325b51 src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Wed Oct 23 16:09:02 2002 +0200
@@ -8,6 +8,30 @@
 
 theory Eval = State + WellType:
 
+
+  -- "Auxiliary notions"
+
+constdefs
+  fits    :: "java_mb prog \<Rightarrow> state \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60)
+ "G,s\<turnstile>a' fits T  \<equiv> case T of PrimT T' \<Rightarrow> False | RefT T' \<Rightarrow> a'=Null \<or> G\<turnstile>obj_ty(lookup_obj s a')\<preceq>T"
+
+constdefs
+  catch ::"java_mb prog \<Rightarrow> xstate \<Rightarrow> cname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60)
+ "G,s\<turnstile>catch C\<equiv>  case abrupt s of None \<Rightarrow> False | Some a \<Rightarrow> G,store s\<turnstile> a fits Class C"
+
+
+
+constdefs
+  lupd       :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state"        ("lupd'(_\<mapsto>_')"[10,10]1000)
+ "lupd vn v   \<equiv> \<lambda> (hp,loc). (hp, (loc(vn\<mapsto>v)))"
+
+constdefs
+  new_xcpt_var :: "vname \<Rightarrow> xstate \<Rightarrow> xstate"
+ "new_xcpt_var vn \<equiv>  \<lambda>(x,s). Norm (lupd(vn\<mapsto>the x) s)"
+
+
+  -- "Evaluation relations"
+
 consts
   eval  :: "java_mb prog => (xstate \<times> expr      \<times> val      \<times> xstate) set"
   evals :: "java_mb prog => (xstate \<times> expr list \<times> val list \<times> xstate) set"