X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fnlibrary%2Fsets%2Fsets.ma;h=7c9bd8d07774f0dab9d0154a09c341d68960601b;hb=062205f9595812819a8783df5b578a5683b27d09;hp=c8f303a6b407920f101126160a4b6d6333d9acfc;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/matita/nlibrary/sets/sets.ma b/matitaB/matita/nlibrary/sets/sets.ma
index c8f303a6b..7c9bd8d07 100644
--- a/matitaB/matita/nlibrary/sets/sets.ma
+++ b/matitaB/matita/nlibrary/sets/sets.ma
@@ -16,46 +16,47 @@
 
 include "logic/connectives.ma".
 
-nrecord powerclass (A: Type[0]) : Type[1] ≝ { mem: A → CProp[0] }.
+record powerclass (A: Type[0]) : Type[1] ≝ { mem: A → CProp[0] }.
 
 interpretation "mem" 'mem a S = (mem ? S a).
 interpretation "powerclass" 'powerset A = (powerclass A).
 interpretation "subset construction" 'subset \eta.x = (mk_powerclass ? x).
 
-ndefinition subseteq ≝ λA.λU,V.∀a:A. a ∈ U → a ∈ V.
+definition subseteq ≝ λA.λU,V.∀a:A. a ∈ U → a ∈ V.
 interpretation "subseteq" 'subseteq U V = (subseteq ? U V).
 
-ndefinition overlaps ≝ λA.λU,V.∃x:A.x ∈ U ∧ x ∈ V.
+definition overlaps ≝ λA.λU,V.∃x:A.x ∈ U ∧ x ∈ V.
 interpretation "overlaps" 'overlaps U V = (overlaps ? U V).
 
-ndefinition intersect ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∧ x ∈ V }.
+definition intersect ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∧ x ∈ V }.
 interpretation "intersect" 'intersects U V = (intersect ? U V).
 
-ndefinition union ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∨ x ∈ V }.
+definition union ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∨ x ∈ V }.
 interpretation "union" 'union U V = (union ? U V).
 
-ndefinition substract ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∧ ¬ x ∈ V }.
+definition substract ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∧ ¬ x ∈ V }.
 interpretation "substract" 'minus U V = (substract ? U V).
 
 
-ndefinition big_union ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∃i. i ∈ T ∧ x ∈ f i }.
+definition big_union ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∃i. i ∈ T ∧ x ∈ f i }.
 
-ndefinition big_intersection ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∀i. i ∈ T → x ∈ f i }.
+definition big_intersection ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∀i. i ∈ T → x ∈ f i }.
 
-ndefinition full_set: ∀A. Ω^A ≝ λA.{ x | True }.
+definition full_set: ∀A. Ω^A ≝ λA.{ x | True }.
 
-nlemma subseteq_refl: ∀A.∀S: Ω^A. S ⊆ S.
-//.nqed.
+lemma subseteq_refl: ∀A.∀S: Ω^A. S ⊆ S.
+//.qed.
 
-nlemma subseteq_trans: ∀A.∀S,T,U: Ω^A. S ⊆ T → T ⊆ U → S ⊆ U.
-/3/.nqed.
+lemma subseteq_trans: ∀A.∀S,T,U: Ω^A. S ⊆ T → T ⊆ U → S ⊆ U.
+/3/.qed.
 
 include "properties/relations1.ma".
 
-ndefinition seteq: ∀A. equivalence_relation1 (Ω^A).
-#A; @(λS,S'. S ⊆ S' ∧ S' ⊆ S); /2/; ##[ #A B; *; /3/]
-#S T U; *; #H1 H2; *; /4/;
-nqed.
+definition seteq: ∀A. equivalence_relation1 (Ω^A).
+#A % [@(λS,S'. S ⊆ S' ∧ S' ⊆ S)]
+/2/[ #A #B * /3/]
+#S #T #U * #H1 #H2 * /4/
+qed.
 
 include "sets/setoids1.ma".