--- 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
--- 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