src/HOL/MicroJava/BV/Correct.thy
changeset 60773 d09c66a0ea10
parent 59199 cb8e5f7a5e4a
child 61361 8b5f00202e1a
     1.1 --- a/src/HOL/MicroJava/BV/Correct.thy	Thu Jul 23 16:40:47 2015 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Jul 23 22:13:42 2015 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4       correct_frames G hp phi rT sig frs))))"
     1.5  
     1.6  definition correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
     1.7 -                  ("_,_ |-JVM _ [ok]"  [51,51] 50) where
     1.8 +                  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50) where
     1.9  "correct_state G phi == \<lambda>(xp,hp,frs).
    1.10     case xp of
    1.11       None \<Rightarrow> (case frs of
    1.12 @@ -59,10 +59,6 @@
    1.13     | Some x \<Rightarrow> frs = []" 
    1.14  
    1.15  
    1.16 -notation (xsymbols)
    1.17 - correct_state  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
    1.18 -
    1.19 -
    1.20  lemma sup_ty_opt_OK:
    1.21    "(G \<turnstile> X <=o (OK T')) = (\<exists>T. X = OK T \<and> G \<turnstile> T \<preceq> T')"
    1.22    by (cases X) auto