# HG changeset patch
# User wenzelm
# Date 963773717 -7200
# Node ID e783491b9a1f43c33664d3578e37b373e1d38eb6
# Parent  86b48eafc70d23fed6caa77db79b38f3ca1fd334
fixed tuple translations;

diff -r 86b48eafc70d -r e783491b9a1f src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Transition.thy	Sun Jul 16 20:54:38 2000 +0200
+++ b/src/HOL/IMP/Transition.thy	Sun Jul 16 20:55:17 2000 +0200
@@ -20,13 +20,13 @@
 
 translations
   "cs0 -1-> cs1"	== "(cs0,cs1) : evalc1"
-  "cs0 -1-> (c1,s1)"	<= "cs0 -1-> (_args c1 s1)"
+  "cs0 -1-> (c1,s1)"	== "(cs0,c1,s1) : evalc1"
 
   "cs0 -n-> cs1" 	== "(cs0,cs1) : evalc1^n"
-  "cs0 -n-> (c1,s1)" 	<= "cs0 -n-> (_args c1 s1)"
+  "cs0 -n-> (c1,s1)" 	== "(cs0,c1,s1) : evalc1^n"
 
   "cs0 -*-> cs1" 	== "(cs0,cs1) : evalc1^*"
-  "cs0 -*-> (c1,s1)" 	<= "cs0 -*-> (_args c1 s1)"
+  "cs0 -*-> (c1,s1)" 	== "(cs0,c1,s1) : evalc1^*"
 
 
 inductive evalc1
diff -r 86b48eafc70d -r e783491b9a1f src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Sun Jul 16 20:54:38 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Sun Jul 16 20:55:17 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