Tests enabled again.

diff --git a/helm/software/matita/library/freescale/table_HC05_tests.ma b/helm/software/matita/library/freescale/table_HC05_tests.ma
index 50f8057039ce3de5f2b2d421f4fef6fc301ed632..fc36c4dbce64f62f61f4e0a28b512fb34b0119a2 100644 (file)
--- a/helm/software/matita/library/freescale/table_HC05_tests.ma
+++ b/helm/software/matita/library/freescale/table_HC05_tests.ma
@@ -85,11 +85,9 @@ lemma ok_mode_table_HC05 : forall_instr_mode (λi.
  reflexivity.
 qed.
 
-(*
 lemma ok_OpIm_table_HC05 :
  forall_instr_mode (λi:instr_mode.
  forall_opcode     (λop:opcode.
   leb (get_OpIm_count HC05 (anyOP HC05 op) i 0 opcode_table_HC05) 1)) = true.
  reflexivity.
 qed.
-*)

diff --git a/helm/software/matita/library/freescale/table_HC08_tests.ma b/helm/software/matita/library/freescale/table_HC08_tests.ma
index d8981d61af1a6676aa346b7888cb59ee7f0c0332..3a6ccc77736f859e13a103b3e57525e680b6b639 100644 (file)
--- a/helm/software/matita/library/freescale/table_HC08_tests.ma
+++ b/helm/software/matita/library/freescale/table_HC08_tests.ma
@@ -114,11 +114,9 @@ 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.
-*)

diff --git a/helm/software/matita/library/freescale/table_HCS08_tests.ma b/helm/software/matita/library/freescale/table_HCS08_tests.ma
index 277b8197bf9adaa27c434d13fe6eee8303590c2e..d19136d1b5d9868262087e2901eb805e75ed6257 100644 (file)
--- a/helm/software/matita/library/freescale/table_HCS08_tests.ma
+++ b/helm/software/matita/library/freescale/table_HCS08_tests.ma
@@ -109,11 +109,9 @@ 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.
-*)

diff --git a/helm/software/matita/library/freescale/table_RS08_tests.ma b/helm/software/matita/library/freescale/table_RS08_tests.ma
index 0ad95525eb02a07dd8cc09fde983079dd5581215..8fbc0cfeafc1021d6c1cd5aa24f20a047eaa4e37 100644 (file)
--- a/helm/software/matita/library/freescale/table_RS08_tests.ma
+++ b/helm/software/matita/library/freescale/table_RS08_tests.ma
@@ -69,11 +69,9 @@ lemma ok_mode_table_RS08 : forall_instr_mode (λi.
  reflexivity.
 qed.
 
-(*
 lemma ok_OpIm_table_RS08 :
  forall_instr_mode (λi:instr_mode.
  forall_opcode     (λop:opcode.
   leb (get_OpIm_count RS08 (anyOP RS08 op) i 0 opcode_table_RS08) 1)) = true.
  reflexivity.
 qed.
-*)