--- a/src/HOL/MicroJava/J/Eval.thy Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy Tue Jun 12 14:11:00 2001 +0200
@@ -13,7 +13,7 @@
evals :: "java_mb prog => (xstate \<times> expr list \<times> val list \<times> xstate) set"
exec :: "java_mb prog => (xstate \<times> stmt \<times> xstate) set"
-syntax
+syntax (xsymbols)
eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
("_ \<turnstile> _ -_\<succ>_-> _" [51,82,60,82,82] 81)
evals:: "[java_mb prog,xstate,expr list,
@@ -22,7 +22,7 @@
exec :: "[java_mb prog,xstate,stmt, xstate] => bool "
("_ \<turnstile> _ -_-> _" [51,82,60,82] 81)
-syntax (HTML)
+syntax
eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
("_ |- _ -_>_-> _" [51,82,60,82,82] 81)
evals:: "[java_mb prog,xstate,expr list,