From 7bb64ff8dba4525e069bab692e67b1cda4be9e1d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 4 Sep 2008 13:37:51 +0000 Subject: [PATCH] .... --- .../matita/library/formal_topology/concrete_spaces.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma index 0fc4d365b..9885a6673 100644 --- a/helm/software/matita/library/formal_topology/concrete_spaces.ma +++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma @@ -66,7 +66,7 @@ qed. interpretation "fintersectsS" 'fintersects U V = (fintersectsS _ U V). - +(* definition relS: ∀o: basic_pair. concr o → Ω \sup (form o) → CProp. @@ -146,4 +146,4 @@ definition CSPA: category. | ] - |*) \ No newline at end of file + |*) -- 2.39.2