# HG changeset patch
# User kleing
# Date 969632884 -7200
# Node ID 4522e59b7d8466460d77bd4375d39deae010ce32
# Parent  f56da476935539a733c0cf8e79ce9f3b78ec89b7
added HTML syntax

diff -r f56da4769355 -r 4522e59b7d84 src/HOL/MicroJava/BV/Convert.thy
--- 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" 
diff -r f56da4769355 -r 4522e59b7d84 src/HOL/MicroJava/BV/Correct.thy
--- 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)
diff -r f56da4769355 -r 4522e59b7d84 src/HOL/MicroJava/JVM/JVMExec.thy
--- 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)