X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Ftable_HC05.ma;h=6938cd3e67da4da6fb181a09de9fac379801195b;hb=84b0d9386906e5bf13bf3d0e6ea736e05ac9e8b8;hp=e0c9b33e750f87123c006b01dc57fbd3afad4648;hpb=7abdf2f1764ba67a48f0829f7a9813ce7426b0c6;p=helm.git

diff --git a/helm/software/matita/library/freescale/table_HC05.ma b/helm/software/matita/library/freescale/table_HC05.ma
index e0c9b33e7..6938cd3e6 100644
--- a/helm/software/matita/library/freescale/table_HC05.ma
+++ b/helm/software/matita/library/freescale/table_HC05.ma
@@ -239,21 +239,21 @@ definition opcode_table_HC05_17 ≝
 
 definition opcode_table_HC05_18 ≝
 [
-  quadrupleT ???? (anyOP HC05 JMP) MODE_DIR1 (Byte 〈xB,xC〉) 〈x0,x2〉
-; quadrupleT ???? (anyOP HC05 JMP) MODE_DIR2 (Byte 〈xC,xC〉) 〈x0,x3〉
-; quadrupleT ???? (anyOP HC05 JMP) MODE_IX2  (Byte 〈xD,xC〉) 〈x0,x4〉
-; quadrupleT ???? (anyOP HC05 JMP) MODE_IX1  (Byte 〈xE,xC〉) 〈x0,x3〉
-; quadrupleT ???? (anyOP HC05 JMP) MODE_IX0  (Byte 〈xF,xC〉) 〈x0,x2〉
+  quadrupleT ???? (anyOP HC05 JMP) MODE_IMM1EXT  (Byte 〈xB,xC〉) 〈x0,x2〉
+; quadrupleT ???? (anyOP HC05 JMP) MODE_IMM2     (Byte 〈xC,xC〉) 〈x0,x3〉
+; quadrupleT ???? (anyOP HC05 JMP) MODE_INHX2ADD (Byte 〈xD,xC〉) 〈x0,x4〉
+; quadrupleT ???? (anyOP HC05 JMP) MODE_INHX1ADD (Byte 〈xE,xC〉) 〈x0,x3〉
+; quadrupleT ???? (anyOP HC05 JMP) MODE_INHX0ADD (Byte 〈xF,xC〉) 〈x0,x2〉
 ].
 
 definition opcode_table_HC05_19 ≝
 [
-  quadrupleT ???? (anyOP HC05 BSR) MODE_IMM1 (Byte 〈xA,xD〉) 〈x0,x6〉
-; quadrupleT ???? (anyOP HC05 JSR) MODE_DIR1 (Byte 〈xB,xD〉) 〈x0,x5〉
-; quadrupleT ???? (anyOP HC05 JSR) MODE_DIR2 (Byte 〈xC,xD〉) 〈x0,x6〉
-; quadrupleT ???? (anyOP HC05 JSR) MODE_IX2  (Byte 〈xD,xD〉) 〈x0,x7〉
-; quadrupleT ???? (anyOP HC05 JSR) MODE_IX1  (Byte 〈xE,xD〉) 〈x0,x6〉
-; quadrupleT ???? (anyOP HC05 JSR) MODE_IX0  (Byte 〈xF,xD〉) 〈x0,x5〉
+  quadrupleT ???? (anyOP HC05 BSR) MODE_IMM1     (Byte 〈xA,xD〉) 〈x0,x6〉
+; quadrupleT ???? (anyOP HC05 JSR) MODE_IMM1EXT  (Byte 〈xB,xD〉) 〈x0,x5〉
+; quadrupleT ???? (anyOP HC05 JSR) MODE_IMM2     (Byte 〈xC,xD〉) 〈x0,x6〉
+; quadrupleT ???? (anyOP HC05 JSR) MODE_INHX2ADD (Byte 〈xD,xD〉) 〈x0,x7〉
+; quadrupleT ???? (anyOP HC05 JSR) MODE_INHX1ADD (Byte 〈xE,xD〉) 〈x0,x6〉
+; quadrupleT ???? (anyOP HC05 JSR) MODE_INHX0ADD (Byte 〈xF,xD〉) 〈x0,x5〉
 ].
 
 definition opcode_table_HC05_20 ≝
@@ -378,4 +378,3 @@ definition opcode_table_HC05 ≝
  opcode_table_HC05_21 @ opcode_table_HC05_22 @ opcode_table_HC05_23 @ opcode_table_HC05_24 @
  opcode_table_HC05_25 @ opcode_table_HC05_26 @ opcode_table_HC05_27 @ opcode_table_HC05_28 @
  opcode_table_HC05_29 @ opcode_table_HC05_30 @ opcode_table_HC05_31.
-