X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Flogic%2Fconnectives.ma;h=026e9216951c9224737b6493953317effd635369;hb=3d3d0248bf4770c63361f7805d2099b2a607f44d;hp=6eb2375dcc895b3b8e4e6068572345382f349e34;hpb=a17430d258e886b5164fca3d65ee7da7c40e6a36;p=helm.git

diff --git a/helm/software/matita/nlibrary/logic/connectives.ma b/helm/software/matita/nlibrary/logic/connectives.ma
index 6eb2375dc..026e92169 100644
--- a/helm/software/matita/nlibrary/logic/connectives.ma
+++ b/helm/software/matita/nlibrary/logic/connectives.ma
@@ -18,9 +18,6 @@ ninductive True: CProp ≝
   I : True.
 
 ninductive False: CProp ≝.
-(* elimination principle *)
-ndefinition False_rect ≝ λP: False → Type.λp: False.
- match p in False return λp. P p with [].
 
 ndefinition Not: CProp → CProp ≝
   λA. A → False.
@@ -42,3 +39,18 @@ ninductive Ex (A:Type) (P:A → CProp) : CProp ≝
     ex_intro: ∀x:A. P x → Ex A P.
 
 interpretation "exists" 'exists x = (Ex ? x).
+
+nrecord iff (A,B: CProp) : CProp ≝
+ { if: A → B;
+   fi: B → A
+ }.
+
+notation > "hvbox(a break \liff b)"
+  left associative with precedence 25
+for @{ 'iff $a $b }.
+
+notation "hvbox(a break \leftrightarrow b)"
+  left associative with precedence 25
+for @{ 'iff $a $b }.
+
+interpretation "logical iff" 'iff x y = (iff x y).