# HG changeset patch
# User oheimb
# Date 965231695 -7200
# Node ID b5d6db4111bca5e58bdd6f94c9f02ee26d008720
# Parent  01d0c66ce52305dcfd2fc5e7809302b7b186dc31
minor corrections

diff -r 01d0c66ce523 -r b5d6db4111bc src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Wed Aug 02 16:49:26 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Wed Aug 02 17:54:55 2000 +0200
@@ -21,12 +21,12 @@
   exec :: "[java_mb prog,xstate,stmt,    xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<rightarrow> _"  [51,82,82,   82]81)
 
 translations
-  "G\\<turnstile>s -e \\<succ> v\\<rightarrow> (x,s')" == "(s, e, v, x, s') \\<in> eval  G"
-  "G\\<turnstile>s -e \\<succ> v\\<rightarrow>    s' " == "(s, e, v,    s') \\<in> eval  G"
-  "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow> (x,s')" == "(s, e, v, x, s') \\<in> evals G"
-  "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow>    s' " == "(s, e, v,    s') \\<in> evals G"
-  "G\\<turnstile>s -c     \\<rightarrow> (x,s')" == "(s, c, x, s') \\<in> exec  G"
-  "G\\<turnstile>s -c     \\<rightarrow>    s' " == "(s, c,    s') \\<in> exec  G"
+  "G\\<turnstile>s -e \\<succ> v\\<rightarrow> (x,s')" <= "(s, e, v, (_args x s')) \\<in> eval  G"
+  "G\\<turnstile>s -e \\<succ> v\\<rightarrow>    s' " == "(s, e, v,          s' ) \\<in> eval  G"
+  "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow> (x,s')" <= "(s, e, v, (_args x s')) \\<in> evals G"
+  "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow>    s' " == "(s, e, v,          s' ) \\<in> evals G"
+  "G\\<turnstile>s -c    \\<rightarrow> (x,s')" <= "(s, c,    (_args x s')) \\<in> exec  G"
+  "G\\<turnstile>s -c    \\<rightarrow>    s' " == "(s, c,             s')  \\<in> exec  G"
 
 inductive "eval G" "evals G" "exec G" intrs
 
@@ -49,7 +49,7 @@
   Lit				   "G\\<turnstile>Norm s -Lit v\\<succ>v\\<rightarrow> Norm s"
 
   BinOp "\\<lbrakk>G\\<turnstile>Norm s -e1\\<succ>v1\\<rightarrow> s1;
-	  G\\<turnstile>s1     -e1\\<succ>v2\\<rightarrow> s2;
+	  G\\<turnstile>s1     -e2\\<succ>v2\\<rightarrow> s2;
 	  v = (case bop of Eq  \\<Rightarrow> Bool (v1 = v2)
 	                 | Add \\<Rightarrow> Intg (the_Intg v1 + the_Intg v2))\\<rbrakk> \\<Longrightarrow>
 				   G\\<turnstile>Norm s -BinOp bop e1 e2\\<succ>v\\<rightarrow> s2"
diff -r 01d0c66ce523 -r b5d6db4111bc src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Wed Aug 02 16:49:26 2000 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Wed Aug 02 17:54:55 2000 +0200
@@ -22,10 +22,8 @@
 
 class Example {
   public static void main (String args[]) {
-    Base e;
-    e=new Ext();
-    try {e.foo(null); }
-    catch (NullPointerException x) {}
+    Base e=new Ext();
+    e.foo(null);
   }
 }
 *)
@@ -91,12 +89,6 @@
 		    Expr(LAcc e..foo({[Class Base]}[Lit Null]))"
 
 
-
-
-
-
-
-
 syntax
 
   NP		:: xcpt
@@ -106,7 +98,7 @@
 
 translations
 
-  "NP"      == "NullPointer"
+  "NP"   == "NullPointer"
   "tprg" == "[ObjectC, BaseC, ExtC]"
   "obj1"    <= "(Ext, empty((vee, Base)\\<mapsto>Bool False)
 			   ((vee, Ext )\\<mapsto>Intg #0))"