--- a/src/HOL/NanoJava/Equivalence.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy Wed Apr 14 14:13:05 2004 +0200
@@ -166,6 +166,8 @@
"MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e>v-n-> t)"
syntax (xsymbols)
MGTe :: "expr => state => etriple" ("MGT\<^sub>e")
+syntax (HTML output)
+ MGTe :: "expr => state => etriple" ("MGT\<^sub>e")
lemma MGF_implies_complete:
"\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"