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=38fccc2b774e493a94eedef76342b56079c0e694;hp=8ab90d06f8632ead2e0146e8fdcf222ff28ece2d;hpb=a687cf5e3e9ae6fb6ead058c4a191002f21fa951;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 8ab90d06f..723ec0b84 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma @@ -15,15 +15,15 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) 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 *) @@ -32,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 ].