New version of freescale:

[helm.git] / helm / software / matita / library / freescale / table_HC08_tests.ma

diff --git a/helm/software/matita/library/freescale/table_HC08_tests.ma b/helm/software/matita/library/freescale/table_HC08_tests.ma
index be7b06b396200878391c9b58e50deedc0a635696..d8981d61af1a6676aa346b7888cb59ee7f0c0332 100644 (file)
--- 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〉
@@ -116,10 +114,11 @@ lemma ok_mode_table_HC08 : forall_instr_mode (λi.
  reflexivity.
 qed.
 
+(*
 lemma ok_OpIm_table_HC08 :
  forall_instr_mode (λi:instr_mode.
  forall_opcode     (λop:opcode.
   leb (get_OpIm_count HC08 (anyOP HC08 op) i 0 opcode_table_HC08) 1)) = true.
  reflexivity.
 qed.
-
+*)