--- a/src/HOL/MicroJava/J/Eval.thy Mon Oct 01 11:56:40 2001 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy Mon Oct 01 13:32:11 2001 +0200
@@ -87,6 +87,7 @@
h' = h(a\<mapsto>(c,(fs((fn,T)\<mapsto>v)))) |] ==>
G\<turnstile>Norm s0 -{T}e1..fn:=e2\<succ>v-> c_hupd h' (x2,s2)"
+
(* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
Call: "[| G\<turnstile>Norm s0 -e\<succ>a'-> s1; a = the_Addr a';
G\<turnstile>s1 -ps[\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
@@ -95,7 +96,6 @@
G\<turnstile> s3 -res\<succ>v -> (x4,s4) |] ==>
G\<turnstile>Norm s0 -{C}e..mn({pTs}ps)\<succ>v-> (x4,(heap s4,l))"
-
(* evaluation of expression lists *)
(* cf. 15.5 *)
@@ -188,4 +188,4 @@
apply (fast)
done
-end
\ No newline at end of file
+end