# HG changeset patch
# User streckem
# Date 1001935931 -7200
# Node ID 352bfe4e1ec020bf4343d5922347560d1d151346
# Parent  0c248bed5225d48fdeee0c3b3acf424c6efe8716
Minor modifications

diff -r 0c248bed5225 -r 352bfe4e1ec0 src/HOL/MicroJava/J/Eval.thy
--- 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