From: Cosimo Oliboni <??>
Date: Sat, 1 Aug 2009 10:49:14 +0000 (+0000)
Subject:  freescale porting, work in progress
X-Git-Tag: make_still_working~3579
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=de7648541633d2b98a65ba340b39494ddb66b28e;p=helm.git

 freescale porting, work in progress
---

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/word16.ma b/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
index 7dd405eeb..86e6629dc 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
@@ -369,7 +369,9 @@ ndefinition w16_to_recw16_aux3 ≝
  ].
 
 nlemma w16_to_recw16_aux4_1 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x1〉〉.
- #n; #e; nelim e; #input; napply (w16_S ? input).
+ #n; #e; nelim e;
+ (* napply (exadecim_ind … e); funziona *)
+ #input; napply (w16_S ? input).
 nqed.
 
 nlemma w16_to_recw16_aux4_2 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x2〉〉.