X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flogic.ma;h=4b90f75181300bdaced20673e08e5d6420f4fbc1;hb=5ca47b58902b9f2583ad1354b860c04ea62df46c;hp=76b4239d4a537037c73ea6649e19fa94c81cdd36;hpb=2199f327081f49b21bdcd23d702b5e07ea4f58ce;p=helm.git

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index 76b4239d4..4b90f7518 100644
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -153,7 +153,7 @@ interpretation "exists on two predicates" 'exists2 x1 x2 = (ex2 ? x1 x2).
 
 lemma ex2_commute: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0.
 #A0 #P0 #P1 * /2 width=3/
-qed.
+qed-.
 
 (* iff *)
 definition iff :=