From: Claudio Sacerdoti Coen Date: Mon, 26 Nov 2007 12:43:17 +0000 (+0000) Subject: Axiom moved from ex_deriv to deriv where it belongs to. X-Git-Tag: make_still_working~5776 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9f04ab7c9b4723d3bebd000d7ff66fed674de465;p=helm.git Axiom moved from ex_deriv to deriv where it belongs to. --- 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: