some more work

[helm.git] / helm / software / matita / contribs / dama / dama_didactic / deriv.ma

diff --git a/helm/software/matita/contribs/dama/dama_didactic/deriv.ma b/helm/software/matita/contribs/dama/dama_didactic/deriv.ma
index 5c2e734c0697037a686f42c3257b25f377a23635..232a91b5e54ffc06d0ac0441d4a1c7426b78d1a7 100644 (file)
--- a/helm/software/matita/contribs/dama/dama_didactic/deriv.ma
+++ b/helm/software/matita/contribs/dama/dama_didactic/deriv.ma
@@ -25,19 +25,15 @@ axiom De: F→F. (*funzione derivata*)
 notation "a '"
   non associative with precedence 80
 for @{ 'deriv $a }.
-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).
 
 notation "hvbox(a break + b)"
   right associative with precedence 45
 for @{ 'oplus $a $b }.
 
-interpretation "function plus" 'plus x y =
- (cic:/matita/didactic/deriv/fplus.con x y).
+interpretation "function plus" 'plus x y = (fplus x y).
 
 axiom i:R→F. (*mappatura  R in F*)
 coercion cic:/matita/didactic/deriv/i.con.
@@ -48,8 +44,7 @@ axiom freflex:F.
 notation "ρ"
   non associative with precedence 100
 for @{ 'rho }.
-interpretation "function flip" 'rho =
- cic:/matita/didactic/deriv/freflex.con.
+interpretation "function flip" 'rho = freflex.
 axiom reflex_ok: ∀f:F. ρ ∘ f = (i (-R1)) · f.
 axiom dereflex: ρ ' = i (-R1). (*Togliere*)
 
@@ -108,7 +103,6 @@ notation "hvbox(a break ^ b)"
   right associative with precedence 75
 for @{ 'elev $a $b }.
  
-interpretation "function power" 'elev x y =
- (cic:/matita/didactic/deriv/felev.con x y). 
+interpretation "function power" 'elev x y = (felev x y). 
 
 axiom tech1: ∀n,m. F_OF_nat n + F_OF_nat m = F_OF_nat (n + m).