freescale porting

[helm.git] / helm / software / matita / contribs / ng_assembly / emulator / model / HC05_model.ma

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/model/HC05_model.ma b/helm/software/matita/contribs/ng_assembly/emulator/model/HC05_model.ma
index 8fbd3da121e3fc2d4cd830ebbdf02593f875173d..33a24f46b3669daf7ad139603b94d54bc53490e3 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/emulator/model/HC05_model.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/model/HC05_model.ma
@@ -43,12 +43,10 @@ ndefinition memory_type_of_FamilyHC05 ≝
  (* etc.. *)
  ].
 
-(* 
-   parametrizzati i non deterministici rispetto a tutti i valori casuali
+(* parametrizzati i non deterministici rispetto a tutti i valori casuali
    che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5).
    l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione
-   (reset V-low), la memoria ed il check possono essere passati
-*)
+   (reset V-low), la memoria ed il check possono essere passati *)
 ndefinition start_of_model_HC05 ≝
 λmcu:HC05_model.λt:memory_impl.
 λmem:aux_mem_type t.λchk:aux_chk_type t.
@@ -78,11 +76,9 @@ ndefinition start_of_model_HC05 ≝
     (*..*)
   ].
 
-(* 
-   cio' che non viene resettato mantiene il valore precedente: nella documentazione
+(* cio' che non viene resettato mantiene il valore precedente: nella documentazione
    viene riportato come "unaffected"/"indeterminate"/"unpredictable"
-   il soft RESET e' diverso da un calo di tensione e la ram non variera'
-*)
+   il soft RESET e' diverso da un calo di tensione e la ram non variera' *)
 ndefinition reset_of_model_HC05 ≝
 λt:memory_impl.λs:any_status HC05 t.
  (mk_any_status HC05 t