--- 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)