removed all the axioms!!!

diff --git a/helm/software/matita/dama/excedence.ma b/helm/software/matita/dama/excedence.ma
index 1bddcb16eabdc9876b0c3219650de8a176485b3d..fa6848e120314b987eaa0f61bf81cec57d42dea6 100644 (file)
--- 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 ae55b5551dae807bd16ab72fae962914c0e70b4d..be941208766b87cf310a3fa3b7d942f7d44d6078 100644 (file)
--- 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)".