X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FNthDerivative.ma;h=180d8a7a2406c909671be36648e71de6e1ba70e0;hb=601baed778a190b580982b588ebe49ba3f762b30;hp=dbcbf20ace9bee1a15d73ddbad4082a144a865dd;hpb=5e01cba364607e7937aec2e359c34f049bb0f108;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma
index dbcbf20ac..180d8a7a2 100644
--- a/helm/software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma
@@ -42,11 +42,11 @@ We now study higher order differentiability.
 We first define what we mean by the derivative of order [n] of a function.
 *)
 
-inline "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/a.var" "Nth_Derivative__".
+alias id "a" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/a.var".
 
-inline "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/b.var" "Nth_Derivative__".
+alias id "b" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/b.var".
 
-inline "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab'.var" "Nth_Derivative__".
+alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab'.var".
 
 (* begin hide *)
 
@@ -88,11 +88,11 @@ Section Trivia
 These are the expected extensionality and uniqueness results.
 *)
 
-inline "cic:/CoRN/ftc/NthDerivative/Trivia/a.var" "Trivia__".
+alias id "a" = "cic:/CoRN/ftc/NthDerivative/Trivia/a.var".
 
-inline "cic:/CoRN/ftc/NthDerivative/Trivia/b.var" "Trivia__".
+alias id "b" = "cic:/CoRN/ftc/NthDerivative/Trivia/b.var".
 
-inline "cic:/CoRN/ftc/NthDerivative/Trivia/Hab'.var" "Trivia__".
+alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Trivia/Hab'.var".
 
 (* begin hide *)
 
@@ -126,11 +126,11 @@ the relation of [n] times derivative, but focus rather on the
 definition of [Diffble_I_n].
 *)
 
-inline "cic:/CoRN/ftc/NthDerivative/Basic_Results/a.var" "Basic_Results__".
+alias id "a" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/a.var".
 
-inline "cic:/CoRN/ftc/NthDerivative/Basic_Results/b.var" "Basic_Results__".
+alias id "b" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/b.var".
 
-inline "cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab'.var" "Basic_Results__".
+alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab'.var".
 
 (* begin hide *)
 
@@ -196,11 +196,11 @@ First order differentiability is just a special case.
 
 (* begin show *)
 
-inline "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/F.var" "Basic_Results__aux__".
+alias id "F" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/F.var".
 
-inline "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffF.var" "Basic_Results__aux__".
+alias id "diffF" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffF.var".
 
-inline "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffFn.var" "Basic_Results__aux__".
+alias id "diffFn" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffFn.var".
 
 (* end show *)
 
@@ -234,11 +234,11 @@ End Basic_Results
 Section More_Results
 *)
 
-inline "cic:/CoRN/ftc/NthDerivative/More_Results/a.var" "More_Results__".
+alias id "a" = "cic:/CoRN/ftc/NthDerivative/More_Results/a.var".
 
-inline "cic:/CoRN/ftc/NthDerivative/More_Results/b.var" "More_Results__".
+alias id "b" = "cic:/CoRN/ftc/NthDerivative/More_Results/b.var".
 
-inline "cic:/CoRN/ftc/NthDerivative/More_Results/Hab'.var" "More_Results__".
+alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/More_Results/Hab'.var".
 
 (* begin hide *)