X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fnlibrary%2FPlogic%2Fconnectives.ma;h=a58c06386524d567eec68eeeab136c56928f10e9;hb=19a25bf176255055193372554437729a6fa1894c;hp=dd3b967cbac2a3efdf338350c24c61c0f46a7c9b;hpb=4e251fb6d7fab1c489c5141759bb896f116b1b91;p=helm.git

diff --git a/matita/matita/nlibrary/Plogic/connectives.ma b/matita/matita/nlibrary/Plogic/connectives.ma
index dd3b967cb..a58c06386 100644
--- a/matita/matita/nlibrary/Plogic/connectives.ma
+++ b/matita/matita/nlibrary/Plogic/connectives.ma
@@ -29,15 +29,15 @@ nmk: (A → False) → Not A.
 interpretation "logical not" 'not x = (Not x).
 
 theorem absurd : ∀ A:Prop. A → ¬A → False.
-#A; #H; #Hn; elim Hn;/2/; qed.
+#A  #H  #Hn  elim Hn /2/  qed.
 
 (*
 ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
-#A; #C; #H; #Hn; nelim (Hn H).
+#A  #C  #H  #Hn  nelim (Hn H).
 nqed. *)
 
 theorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
-/4/; qed.
+/4/  qed.
 
 inductive And (A,B:Prop) : Prop ≝
     conj : A → B → And A B.
@@ -45,11 +45,11 @@ inductive And (A,B:Prop) : Prop ≝
 interpretation "logical and" 'and x y = (And x y).
 
 theorem proj1: ∀A,B:Prop. A ∧ B → A.
-#A; #B; #AB; elim AB; //.
+#A  #B  #AB  elim AB  //.
 qed.
 
 theorem proj2: ∀ A,B:Prop. A ∧ B → B.
-#A; #B; #AB; elim AB; //.
+#A  #B  #AB  elim AB  //.
 qed.
 
 inductive Or (A,B:Prop) : Prop ≝