From 9f04ab7c9b4723d3bebd000d7ff66fed674de465 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 26 Nov 2007 12:43:17 +0000 Subject: [PATCH] Axiom moved from ex_deriv to deriv where it belongs to. --- helm/software/matita/dama_didactic/deriv.ma | 2 ++ helm/software/matita/dama_didactic/ex_deriv.ma | 2 -- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/dama_didactic/deriv.ma b/helm/software/matita/dama_didactic/deriv.ma index 201471c45..9619b94ba 100644 --- a/helm/software/matita/dama_didactic/deriv.ma +++ b/helm/software/matita/dama_didactic/deriv.ma @@ -110,3 +110,5 @@ for @{ 'elev $a $b }. interpretation "function power" 'elev x y = (cic:/matita/didactic/deriv/felev.con x y). + +axiom tech1: ∀n,m. F_OF_nat n + F_OF_nat m = F_OF_nat (n + m). diff --git a/helm/software/matita/dama_didactic/ex_deriv.ma b/helm/software/matita/dama_didactic/ex_deriv.ma index 59e881592..b451a0acc 100644 --- a/helm/software/matita/dama_didactic/ex_deriv.ma +++ b/helm/software/matita/dama_didactic/ex_deriv.ma @@ -183,8 +183,6 @@ theorem dispari_in_pari: ∀ f:F. fdispari f → fpari f '. done. qed. -axiom tech1: ∀n,m. F_OF_nat n + F_OF_nat m = F_OF_nat (n + m). - alias symbol "plus" = "natural plus". alias num (instance 0) = "natural number". theorem de_prodotto_funzioni: -- 2.39.2