--- a/src/HOL/NanoJava/Equivalence.thy Thu Aug 30 15:47:30 2001 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy Thu Aug 30 17:49:46 2001 +0200
@@ -89,7 +89,7 @@
lemma Impl_sound_lemma:
"\<lbrakk>\<forall>z n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (f z ` Ms) (nvalid n);
-M\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z M)"
+Cm\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z Cm)"
by blast
lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l"