src/ZF/Constructible/Rank.thy

--- a/src/ZF/Constructible/Rank.thy	Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/Constructible/Rank.thy	Sat Nov 01 14:20:38 2014 +0100
@@ -566,7 +566,7 @@
 subsubsection{*Ordinal Multiplication*}
 
 lemma omult_eqns_unique:
-     "[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'";
+     "[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'"
 apply (simp add: omult_eqns_def, clarify) 
 apply (erule Ord_cases, simp_all) 
 done