# 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 @@ ("_ \ _ <=' _" [71,71] 70) "sup_state_opt G == lift_bottom (\t t'. G \ 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" - ("_,_\JVM _\" [51,51] 50) + ("_,_ \JVM _ \" [51,51] 50) "correct_state G phi == \(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 \| hp(newref hp \ 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 \ s -jvm-> t == (s,t) \ {(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)