diff -r c06aee15dc00 -r 83cd2140977d src/HOL/NanoJava/Equivalence.thy
--- a/src/HOL/NanoJava/Equivalence.thy	Sun Jan 13 21:14:51 2002 +0100
+++ b/src/HOL/NanoJava/Equivalence.thy	Mon Jan 14 00:16:43 2002 +0100
@@ -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); 
-Cm\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z Cm)"
+  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"