X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fmemory_bits.ma;h=93dcfa53f7f0fa5ff44e14b8eff618044ee71e6f;hb=e607b42a9a469b02ef377210dc34ada14cc603c1;hp=b48a89a3c4a6b2f4b3203c87788b846da6030fc4;hpb=a687cf5e3e9ae6fb6ead058c4a191002f21fa951;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma
index b48a89a3c..93dcfa53f 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          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                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -149,14 +149,14 @@ let newbit7 ≝ match getn_array8T o7 memory_type chk with
  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool old_value)
  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool new_value)
  | MEM_OUT_OF_BOUND ⇒ None bool ] in
-       opt_map ?? newbit0
- (λnb0.opt_map ?? newbit1
- (λnb1.opt_map ?? newbit2
- (λnb2.opt_map ?? newbit3
- (λnb3.opt_map ?? newbit4
- (λnb4.opt_map ?? newbit5
- (λnb5.opt_map ?? newbit6
- (λnb6.opt_map ?? newbit7
+       opt_map … newbit0
+ (λnb0.opt_map … newbit1
+ (λnb1.opt_map … newbit2
+ (λnb2.opt_map … newbit3
+ (λnb3.opt_map … newbit4
+ (λnb4.opt_map … newbit5
+ (λnb5.opt_map … newbit6
+ (λnb6.opt_map … newbit7
  (λnb7.Some ? (mt_update (Array8T bool) mem addr (array_8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))).
 
 (* leggi controllando il tipo di memoria *)
@@ -199,14 +199,14 @@ let newbit7 ≝ match getn_array8T o7 memory_type bit_types with
  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool value)
  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool value)
  | MEM_OUT_OF_BOUND ⇒ None bool ] in
-       opt_map ?? newbit0
- (λnb0.opt_map ?? newbit1
- (λnb1.opt_map ?? newbit2
- (λnb2.opt_map ?? newbit3
- (λnb3.opt_map ?? newbit4
- (λnb4.opt_map ?? newbit5
- (λnb5.opt_map ?? newbit6
- (λnb6.opt_map ?? newbit7
+       opt_map … newbit0
+ (λnb0.opt_map … newbit1
+ (λnb1.opt_map … newbit2
+ (λnb2.opt_map … newbit3
+ (λnb3.opt_map … newbit4
+ (λnb4.opt_map … newbit5
+ (λnb5.opt_map … newbit6
+ (λnb6.opt_map … newbit7
  (λnb7.Some ? (byte8_of_bits (array_8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))).
 
 (* ************************** *)