X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Ftable_HCS08_tests.ma;h=277b8197bf9adaa27c434d13fe6eee8303590c2e;hb=7845d9d0221d94418beecf3d7c3aed3efb2af7fc;hp=011d19313f089a6e576527383222867708770ca5;hpb=25be562c5436746df8d892449a9ff98755c37e9f;p=helm.git

diff --git a/helm/software/matita/library/freescale/table_HCS08_tests.ma b/helm/software/matita/library/freescale/table_HCS08_tests.ma
index 011d19313..277b8197b 100644
--- a/helm/software/matita/library/freescale/table_HCS08_tests.ma
+++ b/helm/software/matita/library/freescale/table_HCS08_tests.ma
@@ -26,8 +26,6 @@
 
 include "freescale/table_HCS08.ma".
 
-(* CORRETTEZZA *)
-
 (* HCS08: opcode non implementati come da manuale (byte) *)
 definition HCS08_not_impl_byte ≝
  [〈x8,xD〉
@@ -111,10 +109,11 @@ lemma ok_mode_table_HCS08 : forall_instr_mode (λi.
  reflexivity.
 qed.
 
+(*
 lemma ok_OpIm_table_HCS08 :
  forall_instr_mode (λi:instr_mode.
  forall_opcode     (λop:opcode.
   leb (get_OpIm_count HCS08 (anyOP HCS08 op) i 0 opcode_table_HCS08) 1)) = true.
  reflexivity.
 qed.
-
+*)