...

[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 0f75a3f2f8be4686dd1390df91e14355c979e8fb..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
@@ -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                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -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.
 *)
+*)