X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FDerivativeOps.ma;h=bd3023428163bad18c54c7728273d3492d9ab5f0;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=b9b7016d3bd729974c289c7fc76ca41f6e4d4b3c;hpb=5e01cba364607e7937aec2e359c34f049bb0f108;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma index b9b7016d3..bd3023428 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma @@ -38,11 +38,11 @@ context.%}.% We begin with some technical stuff that will be necessary for division. *) -inline "cic:/CoRN/ftc/DerivativeOps/Lemmas/a.var" "Lemmas__". +alias id "a" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/a.var". -inline "cic:/CoRN/ftc/DerivativeOps/Lemmas/b.var" "Lemmas__". +alias id "b" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/b.var". -inline "cic:/CoRN/ftc/DerivativeOps/Lemmas/Hab.var" "Lemmas__". +alias id "Hab" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/Hab.var". (* begin hide *) @@ -50,7 +50,7 @@ inline "cic:/CoRN/ftc/DerivativeOps/Lemmas/I.con" "Lemmas__". (* end hide *) -inline "cic:/CoRN/ftc/DerivativeOps/Lemmas/F.var" "Lemmas__". +alias id "F" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/F.var". (* begin hide *) @@ -60,7 +60,7 @@ inline "cic:/CoRN/ftc/DerivativeOps/Lemmas/P.con" "Lemmas__". (* begin show *) -inline "cic:/CoRN/ftc/DerivativeOps/Lemmas/Fbnd.var" "Lemmas__". +alias id "Fbnd" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/Fbnd.var". (* end show *) @@ -83,11 +83,11 @@ Section Local_Results We can now derive all the usual rules for deriving constant and identity functions, sums, inverses and products of functions with a known derivative. *) -inline "cic:/CoRN/ftc/DerivativeOps/Local_Results/a.var" "Local_Results__". +alias id "a" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/a.var". -inline "cic:/CoRN/ftc/DerivativeOps/Local_Results/b.var" "Local_Results__". +alias id "b" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/b.var". -inline "cic:/CoRN/ftc/DerivativeOps/Local_Results/Hab'.var" "Local_Results__". +alias id "Hab'" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/Hab'.var". (* begin hide *) @@ -101,17 +101,17 @@ inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_const.con". inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_id.con". -inline "cic:/CoRN/ftc/DerivativeOps/Local_Results/F.var" "Local_Results__". +alias id "F" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/F.var". -inline "cic:/CoRN/ftc/DerivativeOps/Local_Results/F'.var" "Local_Results__". +alias id "F'" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/F'.var". -inline "cic:/CoRN/ftc/DerivativeOps/Local_Results/G.var" "Local_Results__". +alias id "G" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/G.var". -inline "cic:/CoRN/ftc/DerivativeOps/Local_Results/G'.var" "Local_Results__". +alias id "G'" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/G'.var". -inline "cic:/CoRN/ftc/DerivativeOps/Local_Results/derF.var" "Local_Results__". +alias id "derF" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/derF.var". -inline "cic:/CoRN/ftc/DerivativeOps/Local_Results/derG.var" "Local_Results__". +alias id "derG" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/derG.var". inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_plus.con". @@ -125,7 +125,7 @@ As was the case for continuity, the rule for the reciprocal function has a side (* begin show *) -inline "cic:/CoRN/ftc/DerivativeOps/Local_Results/Fbnd.var" "Local_Results__". +alias id "Fbnd" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/Fbnd.var". (* end show *) @@ -148,11 +148,11 @@ Hint Resolve Derivative_I_const Derivative_I_id Derivative_I_plus Section Corolaries *) -inline "cic:/CoRN/ftc/DerivativeOps/Corolaries/a.var" "Corolaries__". +alias id "a" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/a.var". -inline "cic:/CoRN/ftc/DerivativeOps/Corolaries/b.var" "Corolaries__". +alias id "b" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/b.var". -inline "cic:/CoRN/ftc/DerivativeOps/Corolaries/Hab'.var" "Corolaries__". +alias id "Hab'" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/Hab'.var". (* begin hide *) @@ -162,17 +162,17 @@ inline "cic:/CoRN/ftc/DerivativeOps/Corolaries/I.con" "Corolaries__". (* end hide *) -inline "cic:/CoRN/ftc/DerivativeOps/Corolaries/F.var" "Corolaries__". +alias id "F" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/F.var". -inline "cic:/CoRN/ftc/DerivativeOps/Corolaries/F'.var" "Corolaries__". +alias id "F'" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/F'.var". -inline "cic:/CoRN/ftc/DerivativeOps/Corolaries/G.var" "Corolaries__". +alias id "G" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/G.var". -inline "cic:/CoRN/ftc/DerivativeOps/Corolaries/G'.var" "Corolaries__". +alias id "G'" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/G'.var". -inline "cic:/CoRN/ftc/DerivativeOps/Corolaries/derF.var" "Corolaries__". +alias id "derF" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/derF.var". -inline "cic:/CoRN/ftc/DerivativeOps/Corolaries/derG.var" "Corolaries__". +alias id "derG" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/derG.var". (*#* From this lemmas the rules for the other algebraic operations follow directly. @@ -184,7 +184,7 @@ inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_scal.con". inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_nth.con". -inline "cic:/CoRN/ftc/DerivativeOps/Corolaries/Gbnd.var" "Corolaries__". +alias id "Gbnd" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/Gbnd.var". inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_div.con". @@ -205,13 +205,13 @@ Section Derivative_Sums induction using the constant and addition rules. *) -inline "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/a.var" "Derivative_Sums__". +alias id "a" = "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/a.var". -inline "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/b.var" "Derivative_Sums__". +alias id "b" = "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/b.var". -inline "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/Hab.var" "Derivative_Sums__". +alias id "Hab" = "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/Hab.var". -inline "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/Hab'.var" "Derivative_Sums__". +alias id "Hab'" = "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/Hab'.var". (* begin hide *)