From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 4 Dec 2007 00:05:46 +0000 (+0000)
Subject: removed all the axioms!!!
X-Git-Tag: make_still_working~5740
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5995a1924405fbc2f22d6ac154217b2548878be5;p=helm.git

removed all the axioms!!!
---

diff --git a/helm/software/matita/dama/excedence.ma b/helm/software/matita/dama/excedence.ma
index 1bddcb16e..fa6848e12 100644
--- a/helm/software/matita/dama/excedence.ma
+++ b/helm/software/matita/dama/excedence.ma
@@ -52,7 +52,7 @@ record apartness : Type ≝ {
 }.
 
 notation "a break # b" non associative with precedence 50 for @{ 'apart $a $b}.
-interpretation "axiomatic apartness" 'apart x y = 
+interpretation "apartness" 'apart x y = 
   (cic:/matita/excedence/ap_apart.con _ x y).
 
 definition strong_ext ≝ λA:apartness.λop:A→A.∀x,y. op x # op y → x # y.
diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma
index ae55b5551..be9412087 100644
--- a/helm/software/matita/dama/metric_lattice.ma
+++ b/helm/software/matita/dama/metric_lattice.ma
@@ -122,8 +122,6 @@ interpretation "tends to" 'tends s x =
   (cic:/matita/sequence/tends0.con _ s).    
 *)
 
-axiom core1: ∀G:todgroup.∀e:G.0<e → e/3 + e/2 + e/2 < e.
-
 alias symbol "leq" = "ordered sets less or equal than".
 alias symbol "and" = "constructive and".
 alias symbol "exists" = "constructive exists (Type)".