changeset 61378 | 3e04c9ca001a |
parent 59807 | 22bc39064290 |
child 61990 | 39e4a93ad36e |
--- a/src/HOL/NanoJava/Equivalence.thy Fri Oct 09 19:51:20 2015 +0200 +++ b/src/HOL/NanoJava/Equivalence.thy Fri Oct 09 20:26:03 2015 +0200 @@ -165,8 +165,6 @@ notation (xsymbols) MGTe ("MGT\<^sub>e") -notation (HTML output) - MGTe ("MGT\<^sub>e") lemma MGF_implies_complete: "\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"