src/HOL/MicroJava/JVM/JVMExec.thy
changeset 10042 7164dc0d24d8
parent 9376 c32c5696ec2a
child 10057 8c8d2d0d3ef8
     1.1 --- a/src/HOL/MicroJava/JVM/JVMExec.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  JVMExec = JVMExecInstr + 
     1.5  
     1.6  consts
     1.7 - exec :: "jvm_prog \\<times> jvm_state \\<Rightarrow> jvm_state option"
     1.8 + exec :: "jvm_prog \\<times> jvm_state => jvm_state option"
     1.9  
    1.10  (** exec is not recursive. recdef is just used for pattern matching **)
    1.11  recdef exec "{}"
    1.12 @@ -25,7 +25,7 @@
    1.13  
    1.14  
    1.15  constdefs
    1.16 - exec_all :: "[jvm_prog,jvm_state,jvm_state] \\<Rightarrow> bool"  ("_ \\<turnstile> _ -jvm\\<rightarrow> _" [61,61,61]60)
    1.17 - "G \\<turnstile> s -jvm\\<rightarrow> t \\<equiv> (s,t) \\<in> {(s,t). exec(G,s) = Some t}^*"
    1.18 + exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"  ("_ \\<turnstile> _ -jvm-> _" [61,61,61]60)
    1.19 + "G \\<turnstile> s -jvm-> t == (s,t) \\<in> {(s,t). exec(G,s) = Some t}^*"
    1.20  
    1.21  end