X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ftest_errori.ma;h=4236c5c6341f7c0b93e878951e88b04880244284;hb=d3c72253769956a8af10e6ea990ed34c92999e58;hp=155b6073fe79eb1019284f7f5ba2e0531ad0597f;hpb=2d88fad67eb842ed5fc70cd435f9920c7a2583f8;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/test_errori.ma b/helm/software/matita/contribs/ng_assembly/test_errori.ma
index 155b6073f..4236c5c63 100644
--- a/helm/software/matita/contribs/ng_assembly/test_errori.ma
+++ b/helm/software/matita/contribs/ng_assembly/test_errori.ma
@@ -1,7 +1,6 @@
 
-include "utility/utility.ma".
+(*include "utility/utility.ma".
 
-(*
 nlemma fold_right_neList2_aux3 :
 \forall T. \forall h,h',t,t'.len_neList T (h§§t) = len_neList T (h'§§t') → len_neList T t = len_neList T t'.
  #T; #h; #h'; #t; #t';
@@ -22,9 +21,8 @@ nlemma fold_right_neList2_aux3 :
           nchange in H2:(%) with ((S (len_neList T (a§§l1))) = (S (len_neList T (a§§l))));
 *)
 
-include "freescale/byte8_lemmas.ma".
+(*include "freescale/byte8_lemmas.ma".
 
-(*
 nlemma associative_plusb8_aux
  : \forall e1,e2,e3,e4.
   match plus_ex_d_dc e2 e4 with
@@ -70,9 +68,8 @@ nlemma associative_plusb8
  (*...*)
 *)
 
-include "compiler/ast_type_lemmas.ma".
+(*include "compiler/ast_type_lemmas.ma".
 
-(*
 nlemma symmetric_eqasttype_aux1
  : ∀x1,x2,y2.eq_nat (len_neList ast_type («£x1»)) (len_neList ast_type (x2§§y2)) = false.
  #x1; #x2; #y2; ncases y2; nnormalize;