src/HOL/NanoJava/Equivalence.thy
changeset 14565 c6dc17aab88a
parent 14174 f3cafd2929d5
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/NanoJava/Equivalence.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -166,6 +166,8 @@
     1.4           "MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e>v-n-> t)"
     1.5  syntax (xsymbols)
     1.6           MGTe    :: "expr => state => etriple" ("MGT\<^sub>e")
     1.7 +syntax (HTML output)
     1.8 +         MGTe    :: "expr => state => etriple" ("MGT\<^sub>e")
     1.9  
    1.10  lemma MGF_implies_complete:
    1.11   "\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile>  {P} c {Q} \<Longrightarrow> {} \<turnstile>  {P} c {Q}"