X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Ftable_HC08_tests.ma;h=3a6ccc77736f859e13a103b3e57525e680b6b639;hb=84b0d9386906e5bf13bf3d0e6ea736e05ac9e8b8;hp=be7b06b396200878391c9b58e50deedc0a635696;hpb=7abdf2f1764ba67a48f0829f7a9813ce7426b0c6;p=helm.git

diff --git a/helm/software/matita/library/freescale/table_HC08_tests.ma b/helm/software/matita/library/freescale/table_HC08_tests.ma
index be7b06b39..3a6ccc777 100644
--- a/helm/software/matita/library/freescale/table_HC08_tests.ma
+++ b/helm/software/matita/library/freescale/table_HC08_tests.ma
@@ -26,8 +26,6 @@
 
 include "freescale/table_HC08.ma".
 
-(* CORRETTEZZA *)
-
 (* HC08: opcode non implementati come da manuale (byte) *)
 definition HC08_not_impl_byte ≝
  [〈x3,x2〉;〈x3,xE〉
@@ -122,4 +120,3 @@ lemma ok_OpIm_table_HC08 :
   leb (get_OpIm_count HC08 (anyOP HC08 op) i 0 opcode_table_HC08) 1)) = true.
  reflexivity.
 qed.
-