(no commit message)

[helm.git] / helm / software / matita / contribs / ng_assembly / num / exadecim_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma
index 6e4d25e1ec71e6593fcde7ce685bbd84abf28991..c6e09d5ced0208a43cc77164d9804ab798281e7e 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -27,6 +27,7 @@ include "num/bool_lemmas.ma".
 (* ESADECIMALI *)
 (* *********** *)
 
+(*
 ndefinition exadecim_destruct_aux ≝
 Πe1,e2.ΠP:Prop.ΠH:e1 = e2.
  match eq_ex e1 e2 with [ true ⇒ P → P | false ⇒ P ].
@@ -38,6 +39,7 @@ ndefinition exadecim_destruct : exadecim_destruct_aux.
  nnormalize;
  napply (λx.x).
 nqed.
+*)
 
 nlemma symmetric_andex : symmetricT exadecim exadecim and_ex.
  #e1; #e2;
@@ -314,7 +316,7 @@ nlemma eqex_to_eq : ∀n1,n2.eq_ex n1 n2 = true → n1 = n2.
  ncases n2;
  nnormalize;
  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
  ##]
 nqed.