From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 Nov 2006 21:55:07 +0000 (+0000)
Subject: I have changed the nice notation for derivatives a little bit to always pick
X-Git-Tag: 0.4.95@7852~756
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=45727df35e5ac99ba037318d216210c24ff706ad;p=helm.git

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/matita/library/demo/power_derivative.ma b/matita/library/demo/power_derivative.ma
index ce288b731..879f55d7e 100644
--- a/matita/library/demo/power_derivative.ma
+++ b/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.