X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Ftable_HCS08_tests.ma;h=9880fadb9cdac8497c50264728002e260a1def89;hb=9f580d9bf8f6ba6950b252f587166e95bc8fb1a8;hp=463a3b7a687523927f2560c9712ded95fcef40ff;hpb=f8830ea7f8b308241d73e558092089a24ab2f867;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/table_HCS08_tests.ma b/helm/software/matita/contribs/ng_assembly/freescale/table_HCS08_tests.ma
index 463a3b7a6..9880fadb9 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/table_HCS08_tests.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/table_HCS08_tests.ma
@@ -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 ≝