Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/BV/Correct.thy
changeset 11372 648795477bb5
parent 11252 71c00cb091d2
child 12516 d09d0f160888 
--- a/src/HOL/MicroJava/BV/Correct.thy	Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy	Tue Jun 12 14:11:00 2001 +0200
@@ -56,7 +56,7 @@
 
 constdefs
  correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
-                  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
+                  ("_,_ |-JVM _ [ok]"  [51,51] 50)
 "correct_state G phi == \<lambda>(xp,hp,frs).
    case xp of
      None => (case frs of
@@ -73,9 +73,9 @@
    | Some x => True" 
 
 
-syntax (HTML)
+syntax (xsymbols)
  correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
-                  ("_,_ |-JVM _ [ok]"  [51,51] 50)
+                  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
 
 
 lemma sup_ty_opt_OK:
isabelle