I have changed the nice notation for derivatives a little bit to always pick

'x' as the default variable. This is the only reasonable choice since we already
always pick 'x' for polynoms.

diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma
index ce288b731ad998b959d2c71b8cc74455b79daff9..879f55d7e4976227c48756d39a626a1120d12147 100644 (file)
--- a/helm/software/matita/library/demo/power_derivative.ma
+++ b/helm/software/matita/library/demo/power_derivative.ma
@@ -281,6 +281,7 @@ clear H.
   done.
 qed.
 
+(*
 notation "hvbox(\frac 'd' ('d' ident i) break p)"
   right associative with precedence 90
 for @{ 'derivative ${default
@@ -289,6 +290,14 @@ for @{ 'derivative ${default
 
 interpretation "Rderivative" 'derivative \eta.f =
  (cic:/matita/demo/power_derivative/derivative.con f).
+*)
+
+notation "hvbox(\frac 'd' ('d' 'x') break p)"
+  right associative with precedence 90
+for @{ 'derivative $p}.
+
+interpretation "Rderivative" 'derivative f =
+ (cic:/matita/demo/power_derivative/derivative.con f).
 
 theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n)*x \sup n.
  assume n:nat.