]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/ng_assembly/freescale/table_HCS08_tests.ma
freescale porting, work in progress
[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / table_HCS08_tests.ma
index 463a3b7a687523927f2560c9712ded95fcef40ff..9880fadb9cdac8497c50264728002e260a1def89 100755 (executable)
@@ -42,7 +42,7 @@ nlemma ok_byte_table_HCS08 : forall_byte8 (λb.
  (⊖ (test_not_impl_byte b HCS08_not_impl_byte) ⊙ eq_nat (get_byte_count HCS08 b 0 opcode_table_HCS08) 0))
  = true.
  napply (refl_eq ??).
-qed.
+nqed.
 
 (* HCS08: opcode non implementati come da manuale (0x9E+byte) *)
 ndefinition HCS08_not_impl_word ≝