From 0835fcca50e122239b67fd1eadf13cd88da8f4d2 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 23 Feb 2006 18:15:29 +0000 Subject: [PATCH] information on current compilation state added in each file --- .../matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma | 2 ++ .../matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma | 4 +++- .../matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma | 4 +++- .../matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma | 2 ++ .../matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma | 6 ++++-- .../matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma | 2 ++ helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma | 2 ++ .../matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma | 2 ++ 8 files changed, 20 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma index 3cb239174..62fc8bdfa 100644 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma +++ b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma @@ -12,6 +12,8 @@ (* *) (**************************************************************************) +(* STATO: COMPILA *) + (* Project started Wed Oct 12, 2005 ***************************************) set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_defs". diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma index 7634cbde1..6773470b0 100644 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma +++ b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma @@ -12,6 +12,8 @@ (* *) (**************************************************************************) +(* STATO: NON COMPILA: dev'essere aggiornato *) + set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_eq". include "class_defs.ma". @@ -27,4 +29,4 @@ qed. theorem ceq_sym: \forall C,c1,c2. ceq C c1 c2 \to ceq C c2 c1. intros; elim H; clear H.; auto. qed. -*) \ No newline at end of file +*) diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma index c840fbdaf..1d6c763ab 100644 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma +++ b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma @@ -12,6 +12,8 @@ (* *) (**************************************************************************) +(* STATO: NON COMPILA: attendo che l'oggetto "pippo" venga accettato *) + set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/coa_defs". include "iff.ma". @@ -58,4 +60,4 @@ definition bsup: \forall (P:COA). P \to P \to P \def inductive pippo : Prop \def | Pippo: let x \def zero in zero = x \to pippo. - \ No newline at end of file + diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma index 6c004073e..da2c1f678 100644 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma +++ b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma @@ -12,6 +12,8 @@ (* *) (**************************************************************************) +(* STATO: NON COMPILA: perche' dipende da coa_defs *) + set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/coa_props". include "coa_defs.ma". diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma index ed0afab4f..5bc9c2a7d 100644 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma +++ b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma @@ -12,10 +12,12 @@ (* *) (**************************************************************************) +(* STATO: NON COMPILA: dev'essere aggiornato *) + set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/domain_data". -include "../../library/datatypes/constructors.ma". -include "../../library/datatypes/bool.ma". +include "datatypes/constructors.ma". +include "datatypes/bool.ma". include "domain_defs.ma". (* QUANTIFICATION DOMAINS diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma index 68cbd01fa..dcdf84644 100644 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma +++ b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma @@ -12,6 +12,8 @@ (* *) (**************************************************************************) +(* STATO: COMPILA *) + set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs". include "class_defs.ma". diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma index 9a9491923..0e6205148 100644 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma +++ b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma @@ -12,6 +12,8 @@ (* *) (**************************************************************************) +(* STATO: COMPILA *) + set "baseuri" "cic:/matita/logic/iff". include "../../library/logic/connectives.ma". diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma index 5d872040a..7469f08af 100644 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma +++ b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma @@ -12,6 +12,8 @@ (* *) (**************************************************************************) +(* STATO: NON COMPILA: dev'essere aggiornato *) + set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/subset_defs". include "domain_defs.ma". -- 2.39.2