X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fopcode_base.ma;h=f1bb166b5924938d19b22f870f15d3cecca78368;hb=38fccc2b774e493a94eedef76342b56079c0e694;hp=74b7cc4e278c1575fa6d16acb7430ce3d8413b06;hpb=dc74ed7c4af1aa9b90fc5d2f0a86bd7825696e71;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma
index 74b7cc4e2..f1bb166b5 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma
@@ -15,14 +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/aux_bases.ma".
-include "freescale/word16.ma".
-include "freescale/theory.ma".
+include "num/word16.ma".
 
 (* ********************************************** *)
 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
@@ -124,7 +122,7 @@ ninductive instr_mode: Type ≝
 | MODE_SRT           : bitrigesim → instr_mode
 .
 
-ndefinition eq_instrmode ≝
+ndefinition eq_im ≝
 λi1,i2:instr_mode.
  match i1 with
   [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
@@ -160,7 +158,7 @@ ndefinition eq_instrmode ≝
   | MODE_DIRn n1 ⇒ match i2 with [ MODE_DIRn n2 ⇒ eq_oct n1 n2 | _ ⇒ false ]  
   | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with [ MODE_DIRn_and_IMM1 n2  ⇒ eq_oct n1 n2 | _ ⇒ false ]
   | MODE_TNY e1 ⇒ match i2 with [ MODE_TNY e2 ⇒ eq_ex e1 e2 | _ ⇒ false ]  
-  | MODE_SRT t1 ⇒ match i2 with [ MODE_SRT t2 ⇒ eq_bitrig t1 t2 | _ ⇒ false ]  
+  | MODE_SRT t1 ⇒ match i2 with [ MODE_SRT t2 ⇒ eq_bit t1 t2 | _ ⇒ false ]  
   ].        
 
 (* enumerazione delle istruzioni di tutte le ALU *)