X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fmemory_func.ma;h=723ec0b841aa4aaf1abd6e626ee74a334ebb4b5c;hb=dc7e826399162e2fde3ddf1f02d5530d6cd11205;hp=be27f55478513b6bb891537610f051dac15f3523;hpb=9f580d9bf8f6ba6950b252f587166e95bc8fb1a8;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma
index be27f5547..723ec0b84 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma
@@ -13,21 +13,17 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
-(*                           Progetto FreeScale                           *)
+(*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(* Sviluppato da:                                                         *)
-(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
-(* Questo materiale fa parte della tesi:                                  *)
-(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
-(*                                                                        *)
-(*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
 include "freescale/memory_struct.ma".
-include "freescale/word16.ma".
-include "freescale/option.ma".
-include "freescale/theory.ma".
+include "num/word16.ma".
+include "common/option.ma".
+include "common/list.ma".
 
 (* ********************* *)
 (* MEMORIA E DESCRITTORE *)
@@ -36,7 +32,7 @@ include "freescale/theory.ma".
 (* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *)
 ndefinition mf_check_update_ranged ≝
 λf:word16 → memory_type.λi.λs.λv.
- λx.match in_range x i s with
+ λx.match inrange_w16 x i s with
   [ true ⇒ v
   | false ⇒ f x ].