# HG changeset patch
# User wenzelm
# Date 966876578 -7200
# Node ID 8741740ea6d6cf33178c5eb67d4b90a5d2d44264
# Parent  820cca8573f809b822064be409099c2c3ecd110e
tuned translations;

diff -r 820cca8573f8 -r 8741740ea6d6 src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Mon Aug 21 18:45:29 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Mon Aug 21 18:49:38 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, (_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"
+  "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"
 
 inductive "eval G" "evals G" "exec G" intrs