X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale_tests%2Fmicro_tests.ma;h=6918ba06bdb382085fa298539f583c64dd87de08;hb=dc7e826399162e2fde3ddf1f02d5530d6cd11205;hp=bc9615860d43d11792206367a699ab6db2aa2ef6;hpb=38fccc2b774e493a94eedef76342b56079c0e694;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests.ma b/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests.ma
index bc9615860..6918ba06b 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests.ma
@@ -120,7 +120,7 @@ ndefinition mTest_HCS08_ADC_status ≝
 (* dimostrazione senza svolgimento degli stati, immediata *)
 nlemma ok_mTest_HCS08_ADC_full :
  ∀t:memory_impl.
- execute HCS08 t (TickOK ? (mTest_HCS08_ADC_status t)) 28 =
+ execute HCS08 t (TickOK ? (mTest_HCS08_ADC_status t)) nat28 =
  (* NB: V,N,Z sono tornati false C e' tornato true *)
  TickOK ? (set_pc_reg HCS08 t (* nuovo PC *)
            (set_acc_8_low_reg HCS08 t (mTest_HCS08_ADC_status t) 〈x1,x6〉) (* nuovo A *)
@@ -189,6 +189,8 @@ nlemma ok_mTest_HCS08_ADC_full :
  napply refl_eq.
 nqed.
 
+(* -------------------------------------
+
 (* ********* *)
 (* HCS08 MOV *)
 (* ********* *)
@@ -785,3 +787,4 @@ lemma ok_mTest_bits_MEM_TREE_full :
  reflexivity.
 qed.
 *)
+*)