demodulate takes an extra argument 'all', if present it attempts to solve

[helm.git] / helm / software / matita / library / decidable_kit / decidable.ma

diff --git a/helm/software/matita/library/decidable_kit/decidable.ma b/helm/software/matita/library/decidable_kit/decidable.ma
index 1b2b1fc42423554734d34cd74fa41b544e1fbfdc..3478ef628e44c5871298100c970e3f36c9b05370 100644 (file)
--- a/helm/software/matita/library/decidable_kit/decidable.ma
+++ b/helm/software/matita/library/decidable_kit/decidable.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/decidable_kit/decidable/".
-
 (* classical connectives for decidable properties *)
 
 include "decidable_kit/streicher.ma".
@@ -82,7 +80,7 @@ qed.
 
 lemma andbPF : ∀a,b:bool. reflect (a = false ∨ b = false) (negb (andb a b)).
 intros (a b); apply prove_reflect; cases a; cases b; simplify; intros (H);
-[1,2,3,4: rewrite > H; [1,2:right|3,4:left] reflexivity
+[1,2,3,4: try rewrite > H; [1,2:right|3,4:left] reflexivity
 |5,6,7,8: unfold Not; intros (H1); [2,3,4: destruct H]; cases H1; destruct H2]
 qed.
 
@@ -139,7 +137,7 @@ qed.
 
 lemma leb_eqb : ∀n,m. orb (eqb n m) (leb (S n) m) = leb n m.
 intros (n m); apply bool_to_eq; split; intros (H);
-[1:cases (b2pT ? ? (orbP ? ?) H); [2: autobatch] 
+[1:cases (b2pT ? ? (orbP ? ?) H); [2: autobatch type] 
    rewrite > (eqb_true_to_eq ? ? H1); autobatch
 |2:cases (b2pT ? ? (lebP ? ?) H); 
    [ elim n; [reflexivity|assumption] 
@@ -170,7 +168,7 @@ intros (m n); apply bool_to_eq; split;
 [1: intros; cases (b2pT ? ? (orbP ? ?) H); [1: apply ltbW; assumption]
     rewrite > (eqb_true_to_eq ? ? H1); simplify; 
     rewrite > leb_refl; reflexivity  
-|2: generalize in match m; clear m; elim n 0;
+|2: elim n in m ⊢ % 0;
     [1: simplify; intros; cases n1; reflexivity;
     |2: intros 1 (m); elim m 0;
         [1: intros; apply (p2bT ? ? (orbP ? ?));