From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 18 Dec 2008 13:56:15 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4373
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=52bc8021b8be8fec9c3ae65d6b42c0d92d9c3c74;p=helm.git

...
---

diff --git a/helm/software/matita/library/datatypes/categories.ma b/helm/software/matita/library/datatypes/categories.ma
index 6dac9b044..3a8a6c759 100644
--- a/helm/software/matita/library/datatypes/categories.ma
+++ b/helm/software/matita/library/datatypes/categories.ma
@@ -88,13 +88,6 @@ notation ".= r" with precedence 50 for @{'trans $r}.
 interpretation "trans1" 'trans r = (trans1 _____ r).
 interpretation "trans" 'trans r = (trans _____ r).
 
-(*
-record unary_morphism0 (A,B: setoid) : Type0 ≝
- { fun_0:1> A → B;
-   prop_0: ∀a,a'. eq ? a a' → eq ? (fun_0 a) (fun_0 a')
- }.
-*)
-
 record unary_morphism (A,B: setoid1) : Type0 ≝
  { fun_1:1> A → B;
    prop_1: ∀a,a'. eq1 ? a a' → eq1 ? (fun_1 a) (fun_1 a')
@@ -117,7 +110,6 @@ notation "† c" with precedence 90 for @{'prop1 $c }.
 notation "l ‡ r" with precedence 90 for @{'prop $l $r }.
 notation "#" with precedence 90 for @{'refl}.
 interpretation "prop_1" 'prop1 c = (prop_1 _____ c).
-(* interpretation "prop_0" 'prop1 c = (prop_0 _____ c). *)
 interpretation "prop1" 'prop l r = (prop1 ________ l r).
 interpretation "prop" 'prop l r = (prop ________ l r).
 interpretation "refl1" 'refl = (refl1 ___).
diff --git a/helm/software/matita/library/logic/cprop_connectives.ma b/helm/software/matita/library/logic/cprop_connectives.ma
index c0bbdda18..facda2848 100644
--- a/helm/software/matita/library/logic/cprop_connectives.ma
+++ b/helm/software/matita/library/logic/cprop_connectives.ma
@@ -62,9 +62,17 @@ record Iff (A,B:CProp) : CProp ≝
  { if: A → B;
    fi: B → A
  }.
-
+ 
+record Iff1 (A,B:CProp) : CProp ≝
+ { if1: A → B;
+   fi1: B → A
+ }.
+ 
 interpretation "logical iff" 'iff x y = (Iff x y).
 
+notation "hvbox(a break ⇔ b)" right associative with precedence 25 for @{'iff1 $a $b}.
+interpretation "logical iff type1" 'iff1 x y = (Iff1 x y).
+
 inductive exT (A:Type) (P:A→CProp) : CProp ≝
   ex_introT: ∀w:A. P w → exT A P.