From 84b0d9386906e5bf13bf3d0e6ea736e05ac9e8b8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 14 Mar 2008 12:00:54 +0000 Subject: [PATCH] Tests enabled again. --- helm/software/matita/library/freescale/table_HC05_tests.ma | 2 -- helm/software/matita/library/freescale/table_HC08_tests.ma | 2 -- helm/software/matita/library/freescale/table_HCS08_tests.ma | 2 -- helm/software/matita/library/freescale/table_RS08_tests.ma | 2 -- 4 files changed, 8 deletions(-) diff --git a/helm/software/matita/library/freescale/table_HC05_tests.ma b/helm/software/matita/library/freescale/table_HC05_tests.ma index 50f805703..fc36c4dbc 100644 --- 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 d8981d61a..3a6ccc777 100644 --- 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 277b8197b..d19136d1b 100644 --- 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 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. -*) -- 2.39.2