| changeset 13006 | 51c5f3f11d16 |
| parent 12911 | 704713ca07ea |
| child 13052 | 3bf41c474a88 |
| 13005:42a54d6cec15 | 13006:51c5f3f11d16 |
|---|---|
32 "G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*" |
32 "G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*" |
33 |
33 |
34 |
34 |
35 syntax (xsymbols) |
35 syntax (xsymbols) |
36 exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool" |
36 exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool" |
37 ("_ \<turnstile> _ -jvm-> _" [61,61,61]60) |
37 ("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60) |
38 |
38 |
39 end |
39 end |