X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fopcode_base_lemmas.ma;h=ce4e00642433efa96e0e1aab9fb3361bda074e55;hb=0af747f54642b05b3232319b6ae1753af211dba5;hp=371dc403364fe150da433790b6649b26c9f8f9f0;hpb=dc74ed7c4af1aa9b90fc5d2f0a86bd7825696e71;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma
index 371dc4033..ce4e00642 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma
@@ -15,12 +15,12 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
-include "freescale/bool_lemmas.ma".
+include "num/bool_lemmas.ma".
 include "freescale/opcode_base.ma".
 
 (* ********************************************** *)
@@ -41,25 +41,25 @@ ndefinition mcu_type_destruct : mcu_type_destruct_aux.
  nelim m1;
  ##[ ##1: nelim m2; nnormalize; #H;
           ##[ ##1: napply (λx:P.x)
-          ##| ##*: napply (False_ind (λ_.?) ?);
+          ##| ##*: napply False_ind;
                    nchange with (match HC05 with [ HC05 ⇒ False | _ ⇒ True ]);
                    nrewrite > H; nnormalize; napply I
           ##]
  ##| ##2: nelim m2; nnormalize; #H;
           ##[ ##2: napply (λx:P.x)
-          ##| ##*: napply (False_ind (λ_.?) ?);
+          ##| ##*: napply False_ind;
                    nchange with (match HC08 with [ HC08 ⇒ False | _ ⇒ True ]);
                    nrewrite > H; nnormalize; napply I
           ##]
  ##| ##3: nelim m2; nnormalize; #H;
           ##[ ##3: napply (λx:P.x)
-          ##| ##*: napply (False_ind (λ_.?) ?);
+          ##| ##*: napply False_ind;
                    nchange with (match HCS08 with [ HCS08 ⇒ False | _ ⇒ True ]);
                    nrewrite > H; nnormalize; napply I
           ##]
  ##| ##4: nelim m2; nnormalize; #H;
           ##[ ##4: napply (λx:P.x)
-          ##| ##*: napply (False_ind (λ_.?) ?);
+          ##| ##*: napply False_ind;
                    nchange with (match RS08 with [ RS08 ⇒ False | _ ⇒ True ]);
                    nrewrite > H; nnormalize; napply I
           ##]
@@ -71,7 +71,7 @@ nlemma symmetric_eqmcutype : symmetricT mcu_type bool eq_mcutype.
  nelim m1;
  nelim m2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma eqmcutype_to_eq : ∀m1,m2:mcu_type.(eq_mcutype m1 m2 = true) → (m1 = m2).
@@ -79,8 +79,8 @@ nlemma eqmcutype_to_eq : ∀m1,m2:mcu_type.(eq_mcutype m1 m2 = true) → (m1 = m
  ncases m1;
  ncases m2;
  nnormalize;
- ##[ ##1,6,11,16: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##1,6,11,16: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -89,8 +89,8 @@ nlemma eq_to_eqmcutype : ∀m1,m2.m1 = m2 → eq_mcutype m1 m2 = true.
  ncases m1;
  ncases m2;
  nnormalize;
- ##[ ##1,6,11,16: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (mcu_type_destruct ??? H)
+ ##[ ##1,6,11,16: #H; napply refl_eq
+ ##| ##*: #H; napply (mcu_type_destruct … H)
  ##]
 nqed.
 
@@ -99,7 +99,7 @@ nlemma instr_mode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 →
  nchange with (match MODE_DIRn n2 with [ MODE_DIRn a ⇒ n1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma instr_mode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 = MODE_DIRn_and_IMM1 n2 → n1 = n2.
@@ -107,7 +107,7 @@ nlemma instr_mode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 =
  nchange with (match MODE_DIRn_and_IMM1 n2 with [ MODE_DIRn_and_IMM1 a ⇒ n1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma instr_mode_destruct_MODE_TNY : ∀e1,e2.MODE_TNY e1 = MODE_TNY e2 → e1 = e2.
@@ -115,7 +115,7 @@ nlemma instr_mode_destruct_MODE_TNY : ∀e1,e2.MODE_TNY e1 = MODE_TNY e2 → e1
  nchange with (match MODE_TNY e2 with [ MODE_TNY a ⇒ e1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma instr_mode_destruct_MODE_SRT : ∀t1,t2.MODE_SRT t1 = MODE_SRT t2 → t1 = t2.
@@ -123,5 +123,5 @@ nlemma instr_mode_destruct_MODE_SRT : ∀t1,t2.MODE_SRT t1 = MODE_SRT t2 → t1
  nchange with (match MODE_SRT t2 with [ MODE_SRT a ⇒ t1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.