--- a/src/HOL/MicroJava/J/Eval.thy Fri Sep 22 16:28:04 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy Fri Sep 22 16:28:53 2000 +0200
@@ -16,12 +16,22 @@
syntax
eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
- ("_\\<turnstile>_ -_\\<succ>_-> _"[51,82,82,82,82]81)
+ ("_ \\<turnstile> _ -_\\<succ>_-> _" [51,82,82,82,82] 81)
evals:: "[java_mb prog,xstate,expr list,
val list,xstate] => bool "
- ("_\\<turnstile>_ -_[\\<succ>]_-> _"[51,82,51,51,82]81)
+ ("_ \\<turnstile> _ -_[\\<succ>]_-> _" [51,82,51,51,82] 81)
exec :: "[java_mb prog,xstate,stmt, xstate] => bool "
- ("_\\<turnstile>_ -_-> _" [51,82,82, 82]81)
+ ("_ \\<turnstile> _ -_-> _" [51,82,82,82] 81)
+
+syntax (HTML)
+ eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
+ ("_ |- _ -_>_-> _" [51,82,82,82,82] 81)
+ evals:: "[java_mb prog,xstate,expr list,
+ val list,xstate] => bool "
+ ("_ |- _ -_[>]_-> _" [51,82,51,51,82] 81)
+ exec :: "[java_mb prog,xstate,stmt, xstate] => bool "
+ ("_ |- _ -_-> _" [51,82,82,82] 81)
+
translations
"G\\<turnstile>s -e \\<succ> v-> (x,s')" <= "(s, e, v, x, s') \\<in> eval G"