From 5995a1924405fbc2f22d6ac154217b2548878be5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 4 Dec 2007 00:05:46 +0000
Subject: [PATCH] removed all the axioms!!!

---
 helm/software/matita/dama/excedence.ma      | 2 +-
 helm/software/matita/dama/metric_lattice.ma | 2 --
 2 files changed, 1 insertion(+), 3 deletions(-)

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)".
-- 
2.39.2