X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Ftable_RS08_tests.ma;fp=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Ftable_RS08_tests.ma;h=8fbc0cfeafc1021d6c1cd5aa24f20a047eaa4e37;hb=84b0d9386906e5bf13bf3d0e6ea736e05ac9e8b8;hp=0ad95525eb02a07dd8cc09fde983079dd5581215;hpb=b699884bb9816aa55f9bd0a2d7bffde4dc03c643;p=helm.git

diff --git a/helm/software/matita/library/freescale/table_RS08_tests.ma b/helm/software/matita/library/freescale/table_RS08_tests.ma
index 0ad95525e..8fbc0cfea 100644
--- 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.
-*)