From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 18 Mar 2010 11:36:56 +0000 (+0000)
Subject: Porting alla nuova def. di negazione
X-Git-Tag: make_still_working~2987
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fffc8fda02a15fd60817ab1b828cfd6fe2968a11;p=helm.git

Porting alla nuova def. di negazione
---

diff --git a/helm/software/matita/nlibrary/basics/functions.ma b/helm/software/matita/nlibrary/basics/functions.ma
index a4a8f240d..186aee41d 100644
--- a/helm/software/matita/nlibrary/basics/functions.ma
+++ b/helm/software/matita/nlibrary/basics/functions.ma
@@ -36,11 +36,12 @@ ndefinition symmetric2: ∀A,B:Type[0].∀f:A→A→B.Prop
 ndefinition associative: ∀A:Type[0].∀f:A→A→A.Prop
 ≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z).
 
+(*
 ntheorem eq_f_g_h:
   ∀A,B,C,D:Type[0].∀f:C→D.∀g:B→C.∀h:A→B.
   f∘(g∘h) = (f∘g)∘h.
   //.
-nqed.
+nqed. *)
 
 (* functions and relations *)
 ndefinition monotonic : ∀A:Type.∀R:A→A→Prop.
diff --git a/helm/software/matita/nlibrary/basics/relations.ma b/helm/software/matita/nlibrary/basics/relations.ma
index e70a5877a..9a01823be 100644
--- a/helm/software/matita/nlibrary/basics/relations.ma
+++ b/helm/software/matita/nlibrary/basics/relations.ma
@@ -17,6 +17,9 @@ include "Plogic/connectives.ma".
 ndefinition relation : Type \to Type
 ≝ λA:Type.A→A→Prop. 
 
+nrecord relation (A:Type) : Type ≝
+{fun:2> A→A→Prop}.
+
 ndefinition reflexive: ∀A:Type.∀R :relation A.Prop
 ≝ λA.λR.∀x:A.R x x.