X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fmodel%2FHCS08_model.ma;h=40f928dd43cd0e4c0d679f5db68ae211d69ee840;hb=826883e023c178930ca3dd69567eac23f15ef9c4;hp=71acc536a8d39c3638c38204262824c11be94748;hpb=434258767bd3307ea05d9eab48892a6fff73888d;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/model/HCS08_model.ma b/helm/software/matita/contribs/ng_assembly/emulator/model/HCS08_model.ma
index 71acc536a..40f928dd4 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/model/HCS08_model.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/model/HCS08_model.ma
@@ -50,12 +50,10 @@ ndefinition memory_type_of_FamilyHCS08 ≝
  (* 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_HCS08 ≝
 λmcu:HCS08_model.λt:memory_impl.
 λmem:aux_mem_type t.λchk:aux_chk_type t.
@@ -79,11 +77,9 @@ ndefinition start_of_model_HCS08 ≝
    (* chk *) chk
    (* clk: reset *) (None ?).
 
-(* 
-   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_HCS08 ≝
 λt:memory_impl.λs:any_status HCS08 t.
  (mk_any_status HCS08 t