fixed scripts

diff --git a/helm/software/matita/contribs/didactic/shannon.ma b/helm/software/matita/contribs/didactic/shannon.ma
index 5e1db41e891d7a7bc6d8cff6f2314d6e0c04f8c4..233c323a21016844fd766ac00be9f278a149eab6 100644 (file)
--- a/helm/software/matita/contribs/didactic/shannon.ma
+++ b/helm/software/matita/contribs/didactic/shannon.ma
@@ -557,10 +557,9 @@ DOCEND*)
       = ([[ if true then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v).
       = ([[ (FNot f)[ FBot/x ] ]]_v).
       = ([[ FNot (f[ FBot/x ]) ]]_v).
-      (* FIXME, ASSERT IN PARAMOD = (1 - [[ f[ FBot/x ] ]]_v). = [[ FNot f ]]_v). *)
-      change with (1 - [[ f[ FBot/x ] ]]_v = [[ FNot f ]]_v).
+      = (1 - [[ f[ FBot/x ] ]]_v).
       = (1 - [[ f ]]_v) by H5.
-      change with ([[ FNot f ]]_v = [[ FNot f ]]_v).
+      = ([[ FNot f ]]_v).
     done.
   case Right.
     by H1, H we proved 
@@ -572,9 +571,9 @@ DOCEND*)
       = ([[ if false then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v).
       = ([[ (FNot f)[ FTop/x ] ]]_v).
       = ([[ FNot (f[ FTop/x ]) ]]_v).
-      change with (1 - [[ f[ FTop/x ] ]]_v = [[ FNot f ]]_v) .
+      = (1 - [[ f[ FTop/x ] ]]_v).
       = (1 - [[ f ]]_v) by H5.
-      change with ([[ FNot f ]]_v = [[ FNot f ]]_v).
+      = ([[ FNot f ]]_v).
     done.
 qed.
 

diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma
index 8ab638da8694fe04a6c82d280f12ef7233155e5b..adf85249967c8fe1c402b82dcabbb4839679a44c 100644 (file)
--- a/helm/software/matita/library/demo/power_derivative.ma
+++ b/helm/software/matita/library/demo/power_derivative.ma
@@ -264,10 +264,10 @@ theorem derivative_power: ∀n:nat. D[x \sup n] = n·x \sup (pred n).
     case left.
       suppose (0 < m) (m_pos).
       using (S_pred ? m_pos) we proved (m = 1 + pred m) (H1).
-     done.
+     by H1 done.
     case right.
       suppose (0=m) (m_zero). 
-    done.
+    by m_zero, Fmult_zero_f done.
   conclude
      (D[x \sup (1+m)])
    = (D[x · x \sup m]).