fixed tuple translations;
authorwenzelm
Sun Jul 16 20:55:17 2000 +0200 (2000-07-16)
changeset 9364e783491b9a1f
parent 9363 86b48eafc70d
child 9365 0cced1b20d68
fixed tuple translations;
src/HOL/IMP/Transition.thy
src/HOL/MicroJava/J/Eval.thy
     1.1 --- a/src/HOL/IMP/Transition.thy	Sun Jul 16 20:54:38 2000 +0200
     1.2 +++ b/src/HOL/IMP/Transition.thy	Sun Jul 16 20:55:17 2000 +0200
     1.3 @@ -20,13 +20,13 @@
     1.4  
     1.5  translations
     1.6    "cs0 -1-> cs1"	== "(cs0,cs1) : evalc1"
     1.7 -  "cs0 -1-> (c1,s1)"	<= "cs0 -1-> (_args c1 s1)"
     1.8 +  "cs0 -1-> (c1,s1)"	== "(cs0,c1,s1) : evalc1"
     1.9  
    1.10    "cs0 -n-> cs1" 	== "(cs0,cs1) : evalc1^n"
    1.11 -  "cs0 -n-> (c1,s1)" 	<= "cs0 -n-> (_args c1 s1)"
    1.12 +  "cs0 -n-> (c1,s1)" 	== "(cs0,c1,s1) : evalc1^n"
    1.13  
    1.14    "cs0 -*-> cs1" 	== "(cs0,cs1) : evalc1^*"
    1.15 -  "cs0 -*-> (c1,s1)" 	<= "cs0 -*-> (_args c1 s1)"
    1.16 +  "cs0 -*-> (c1,s1)" 	== "(cs0,c1,s1) : evalc1^*"
    1.17  
    1.18  
    1.19  inductive evalc1
     2.1 --- a/src/HOL/MicroJava/J/Eval.thy	Sun Jul 16 20:54:38 2000 +0200
     2.2 +++ b/src/HOL/MicroJava/J/Eval.thy	Sun Jul 16 20:55:17 2000 +0200
     2.3 @@ -21,12 +21,12 @@
     2.4    exec :: "[java_mb prog,xstate,stmt,    xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<rightarrow> _"  [51,82,82,   82]81)
     2.5  
     2.6  translations
     2.7 -  "G\\<turnstile>s -e \\<succ> v\\<rightarrow> (x,s')" == "(s, e, v, _args x s') \\<in> eval  G"
     2.8 -  "G\\<turnstile>s -e \\<succ> v\\<rightarrow>    s' " == "(s, e, v,         s') \\<in> eval  G"
     2.9 -  "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow> (x,s')" == "(s, e, v, _args x s') \\<in> evals G"
    2.10 -  "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow>    s' " == "(s, e, v,         s') \\<in> evals G"
    2.11 -  "G\\<turnstile>s -c     \\<rightarrow> (x,s')" == "(s, c,    _args x s') \\<in> exec  G"
    2.12 -  "G\\<turnstile>s -c     \\<rightarrow>    s' " == "(s, c,            s') \\<in> exec  G"
    2.13 +  "G\\<turnstile>s -e \\<succ> v\\<rightarrow> (x,s')" == "(s, e, v, x, s') \\<in> eval  G"
    2.14 +  "G\\<turnstile>s -e \\<succ> v\\<rightarrow>    s' " == "(s, e, v,    s') \\<in> eval  G"
    2.15 +  "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow> (x,s')" == "(s, e, v, x, s') \\<in> evals G"
    2.16 +  "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow>    s' " == "(s, e, v,    s') \\<in> evals G"
    2.17 +  "G\\<turnstile>s -c     \\<rightarrow> (x,s')" == "(s, c, x, s') \\<in> exec  G"
    2.18 +  "G\\<turnstile>s -c     \\<rightarrow>    s' " == "(s, c,    s') \\<in> exec  G"
    2.19  
    2.20  inductive "eval G" "evals G" "exec G" intrs
    2.21