freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale_tests / micro_tests.ma

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 bc9615860d43d11792206367a699ab6db2aa2ef6..6918ba06bdb382085fa298539f583c64dd87de08 100755 (executable)
--- 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.
 *)
+*)