--- a/src/HOL/MicroJava/BV/Convert.thy Fri Sep 22 13:16:24 2000 +0200
+++ b/src/HOL/MicroJava/BV/Convert.thy Fri Sep 22 16:28:04 2000 +0200
@@ -62,7 +62,7 @@
("_ \<turnstile> _ <=' _" [71,71] 70)
"sup_state_opt G == lift_bottom (\<lambda>t t'. G \<turnstile> t <=s t')"
-syntax (HTML output)
+syntax (HTML)
sup_ty_opt :: "['code prog,ty err,ty err] => bool"
("_ |- _ <=o _")
sup_loc :: "['code prog,locvars_type,locvars_type] => bool"
--- a/src/HOL/MicroJava/BV/Correct.thy Fri Sep 22 13:16:24 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy Fri Sep 22 16:28:04 2000 +0200
@@ -55,7 +55,7 @@
constdefs
correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
- ("_,_\<turnstile>JVM _\<surd>" [51,51] 50)
+ ("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50)
"correct_state G phi == \<lambda>(xp,hp,frs).
case xp of
None => (case frs of
@@ -71,6 +71,11 @@
| Some x => True"
+syntax (HTML)
+ correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
+ ("_,_ |-JVM _ [ok]" [51,51] 50)
+
+
lemma sup_heap_newref:
"hp x = None ==> hp \<le>| hp(newref hp \<mapsto> obj)"
apply (unfold hext_def)
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Fri Sep 22 13:16:24 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Fri Sep 22 16:28:04 2000 +0200
@@ -32,7 +32,7 @@
"G \<turnstile> s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
-syntax (HTML output)
+syntax (HTML)
exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
("_ |- _ -jvm-> _" [61,61,61]60)