--- a/src/HOL/MicroJava/J/Eval.thy Thu Aug 07 17:46:50 2003 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy Fri Aug 08 14:54:37 2003 +0200
@@ -193,6 +193,13 @@
apply (fast)
done
+lemma exec_no_xcpt: "G \<turnstile> (x, s) -c-> (None, s')
+\<Longrightarrow> x = None"
+apply (drule eval_evals_exec_no_xcpt [THEN conjunct2 [THEN conjunct2], rule_format])
+apply simp+
+done
+
+
lemma eval_evals_exec_xcpt:
"!!s s'. (G\<turnstile>(x,s) -e \<succ> v -> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s) \<and>
(G\<turnstile>(x,s) -es[\<succ>]vs-> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s) \<and>