From 1e8c961814b55b806652b8b8243d6f56108bda9c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 23 Aug 2006 08:04:36 +0000 Subject: [PATCH] new naming --- .../matita/contribs/RELATIONAL/BEq/{BEq.ma => defs.ma} | 2 +- .../matita/contribs/RELATIONAL/BNot/{BNot.ma => defs.ma} | 2 +- .../matita/contribs/RELATIONAL/Bool/{Bool.ma => defs.ma} | 0 .../matita/contribs/RELATIONAL/NLE/{NLE.ma => defs.ma} | 2 +- .../matita/contribs/RELATIONAL/NPlus/{NPlus.ma => defs.ma} | 2 +- .../matita/contribs/RELATIONAL/NPlus/{NPlus_fwd.ma => fwd.ma} | 4 ++-- .../contribs/RELATIONAL/NPlus/{NPlus_props.ma => props.ma} | 2 +- .../matita/contribs/RELATIONAL/Nat/{Nat.ma => defs.ma} | 0 .../matita/contribs/RELATIONAL/Nat/{Nat_fwd.ma => fwd.ma} | 2 +- 9 files changed, 8 insertions(+), 8 deletions(-) rename helm/software/matita/contribs/RELATIONAL/BEq/{BEq.ma => defs.ma} (98%) rename helm/software/matita/contribs/RELATIONAL/BNot/{BNot.ma => defs.ma} (97%) rename helm/software/matita/contribs/RELATIONAL/Bool/{Bool.ma => defs.ma} (100%) rename helm/software/matita/contribs/RELATIONAL/NLE/{NLE.ma => defs.ma} (98%) rename helm/software/matita/contribs/RELATIONAL/NPlus/{NPlus.ma => defs.ma} (98%) rename helm/software/matita/contribs/RELATIONAL/NPlus/{NPlus_fwd.ma => fwd.ma} (98%) rename helm/software/matita/contribs/RELATIONAL/NPlus/{NPlus_props.ma => props.ma} (99%) rename helm/software/matita/contribs/RELATIONAL/Nat/{Nat.ma => defs.ma} (100%) rename helm/software/matita/contribs/RELATIONAL/Nat/{Nat_fwd.ma => fwd.ma} (98%) diff --git a/helm/software/matita/contribs/RELATIONAL/BEq/BEq.ma b/helm/software/matita/contribs/RELATIONAL/BEq/defs.ma similarity index 98% rename from helm/software/matita/contribs/RELATIONAL/BEq/BEq.ma rename to helm/software/matita/contribs/RELATIONAL/BEq/defs.ma index 3d40598f0..0b52af116 100644 --- a/helm/software/matita/contribs/RELATIONAL/BEq/BEq.ma +++ b/helm/software/matita/contribs/RELATIONAL/BEq/defs.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/RELATIONAL/BEq/defs". include "logic/equality.ma". -include "BNot/BNot.ma". +include "BNot/defs.ma". inductive BEq (b1:Bool): Bool \to Bool \to Prop \def | beq_false: \forall b2. BNot b1 b2 \to BEq b1 false b2 diff --git a/helm/software/matita/contribs/RELATIONAL/BNot/BNot.ma b/helm/software/matita/contribs/RELATIONAL/BNot/defs.ma similarity index 97% rename from helm/software/matita/contribs/RELATIONAL/BNot/BNot.ma rename to helm/software/matita/contribs/RELATIONAL/BNot/defs.ma index f83a3c8ca..d62264513 100644 --- a/helm/software/matita/contribs/RELATIONAL/BNot/BNot.ma +++ b/helm/software/matita/contribs/RELATIONAL/BNot/defs.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/RELATIONAL/BNot/defs". -include "Bool/Bool.ma". +include "Bool/defs.ma". inductive BNot: Bool \to Bool \to Prop \def | bnot_false: BNot false true diff --git a/helm/software/matita/contribs/RELATIONAL/Bool/Bool.ma b/helm/software/matita/contribs/RELATIONAL/Bool/defs.ma similarity index 100% rename from helm/software/matita/contribs/RELATIONAL/Bool/Bool.ma rename to helm/software/matita/contribs/RELATIONAL/Bool/defs.ma diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/NLE.ma b/helm/software/matita/contribs/RELATIONAL/NLE/defs.ma similarity index 98% rename from helm/software/matita/contribs/RELATIONAL/NLE/NLE.ma rename to helm/software/matita/contribs/RELATIONAL/NLE/defs.ma index 29d15e2ab..19e45c3bc 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/NLE.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/defs.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/defs". -include "Nat/Nat.ma". +include "Nat/defs.ma". inductive NLE: Nat \to Nat \to Prop \def | NLE_zero: \forall q. NLE zero q diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/NPlus.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma similarity index 98% rename from helm/software/matita/contribs/RELATIONAL/NPlus/NPlus.ma rename to helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma index 271bce10b..92561bc5c 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/NPlus.ma +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/RELATIONAL/NPlus/defs". include "logic/equality.ma". -include "Nat/Nat.ma". +include "Nat/defs.ma". inductive NPlus (p:Nat): Nat \to Nat \to Prop \def | nplus_zero_2: NPlus p zero p diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/NPlus_fwd.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma similarity index 98% rename from helm/software/matita/contribs/RELATIONAL/NPlus/NPlus_fwd.ma rename to helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma index d6de420e2..bae48d405 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/NPlus_fwd.ma +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma @@ -14,8 +14,8 @@ set "baseuri" "cic:/matita/RELATIONAL/NPlus/fwd". -include "Nat/Nat_fwd.ma". -include "NPlus/NPlus.ma". +include "Nat/fwd.ma". +include "NPlus/defs.ma". (* primitive generation lemmas proved by elimination and inversion *) diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/NPlus_props.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/props.ma similarity index 99% rename from helm/software/matita/contribs/RELATIONAL/NPlus/NPlus_props.ma rename to helm/software/matita/contribs/RELATIONAL/NPlus/props.ma index eb580c983..56146a3bf 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/NPlus_props.ma +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/props.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/RELATIONAL/NPlus/props". -include "NPlus/NPlus_fwd.ma". +include "NPlus/fwd.ma". theorem nplus_zero_1: \forall q. NPlus zero q q. intros. elim q; clear q; auto. diff --git a/helm/software/matita/contribs/RELATIONAL/Nat/Nat.ma b/helm/software/matita/contribs/RELATIONAL/Nat/defs.ma similarity index 100% rename from helm/software/matita/contribs/RELATIONAL/Nat/Nat.ma rename to helm/software/matita/contribs/RELATIONAL/Nat/defs.ma diff --git a/helm/software/matita/contribs/RELATIONAL/Nat/Nat_fwd.ma b/helm/software/matita/contribs/RELATIONAL/Nat/fwd.ma similarity index 98% rename from helm/software/matita/contribs/RELATIONAL/Nat/Nat_fwd.ma rename to helm/software/matita/contribs/RELATIONAL/Nat/fwd.ma index 28c8733cb..09847de2e 100644 --- a/helm/software/matita/contribs/RELATIONAL/Nat/Nat_fwd.ma +++ b/helm/software/matita/contribs/RELATIONAL/Nat/fwd.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/RELATIONAL/Nat/fwd". include "logic/equality.ma". -include "Nat/Nat.ma". +include "Nat/defs.ma". theorem eq_gen_zero_succ: \forall (P:Prop). \forall m2. zero = succ m2 \to P. intros. discriminate H. -- 2.39.2