-interpretation "function derivative" 'deriv x =
- (cic:/matita/didactic/deriv/De.con x).
-interpretation "function mult" 'mult x y =
- (cic:/matita/didactic/deriv/fmult.con x y).
-interpretation "function compositon" 'compose x y =
- (cic:/matita/didactic/deriv/fcomp.con x y).
+interpretation "function derivative" 'deriv x = (De x).
+interpretation "function mult" 'mult x y = (fmult x y).
+interpretation "function compositon" 'compose x y = (fcomp x y).