X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2FPlogic%2Fconnectives.ma;h=bf17771fb9890a632f0f49f2b8e223837712f36a;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=84bd36454064e90ba35f74df324a28cb8407f83f;hpb=ee1df68d10351f30ea591ccc2173197d99e307cc;p=helm.git

diff --git a/helm/software/matita/nlibrary/Plogic/connectives.ma b/helm/software/matita/nlibrary/Plogic/connectives.ma
index 84bd36454..bf17771fb 100644
--- a/helm/software/matita/nlibrary/Plogic/connectives.ma
+++ b/helm/software/matita/nlibrary/Plogic/connectives.ma
@@ -30,8 +30,6 @@ ndefinition Not: Prop → Prop ≝
 ninductive Not (A:Prop): Prop ≝
 nmk: (A → False) → Not A.
 
-ncheck Not_ind.
-
 interpretation "logical not" 'not x = (Not x).
 
 ntheorem absurd : ∀ A:Prop. A → ¬A → False.
@@ -77,3 +75,5 @@ ninductive ex2 (A:Type[0]) (P,Q:A \to Prop) : Prop ≝
 
 ndefinition iff :=
  λ A,B. (A → B) ∧ (B → A).
+
+interpretation "iff" 'iff a b = (iff a b).