--- a/src/HOL/MicroJava/JVM/JVMExec.thy Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Tue Jun 12 14:11:00 2001 +0200
@@ -28,12 +28,12 @@
constdefs
exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
- ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
- "G \<turnstile> s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
+ ("_ |- _ -jvm-> _" [61,61,61]60)
+ "G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
-syntax (HTML)
+syntax (xsymbols)
exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
- ("_ |- _ -jvm-> _" [61,61,61]60)
+ ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
end