New syntax for auto-related tactics and conclude/obtain.

[helm.git] / helm / software / matita / library / freescale / translation.ma

diff --git a/helm/software/matita/library/freescale/translation.ma b/helm/software/matita/library/freescale/translation.ma
index dae2b5fd511a6b11ed22e1fe060f9fc417c00c41..0463cff55a25cf15797f17560fa496b5d7183495 100644 (file)
--- a/helm/software/matita/library/freescale/translation.ma
+++ b/helm/software/matita/library/freescale/translation.ma
@@ -24,15 +24,9 @@
 (*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
-set "baseuri" "cic:/matita/freescale/translation/".
-
-(*include "/media/VIRTUOSO/freescale/table_HC05.ma".*)
 include "freescale/table_HC05.ma".
-(*include "/media/VIRTUOSO/freescale/table_HC08.ma".*)
 include "freescale/table_HC08.ma".
-(*include "/media/VIRTUOSO/freescale/table_HCS08.ma".*)
 include "freescale/table_HCS08.ma".
-(*include "/media/VIRTUOSO/freescale/table_RS08.ma".*)
 include "freescale/table_RS08.ma".
 
 (* ***************************** *)
@@ -87,7 +81,11 @@ inductive MA_check : instr_mode → Type ≝
 | maINHA             : MA_check MODE_INHA
 | maINHX             : MA_check MODE_INHX
 | maINHH             : MA_check MODE_INHH
+| maINHX0ADD         : MA_check MODE_INHX0ADD
+| maINHX1ADD         : byte8 → MA_check MODE_INHX1ADD
+| maINHX2ADD         : word16 → MA_check MODE_INHX2ADD
 | maIMM1             : byte8  → MA_check MODE_IMM1
+| maIMM1EXT          : byte8  → MA_check MODE_IMM1EXT
 | maIMM2             : word16 → MA_check MODE_IMM2
 | maDIR1             : byte8  → MA_check MODE_DIR1
 | maDIR2             : word16 → MA_check MODE_DIR2
@@ -131,8 +129,13 @@ definition args_picker ≝
   | maINHA   ⇒ nil ? 
   | maINHX   ⇒ nil ? 
   | maINHH   ⇒ nil ?
+  (* inherent address: legale se nessun operando/1 byte/1 word *)
+  | maINHX0ADD ⇒ nil ?
+  | maINHX1ADD b ⇒ [ TByte m b ]
+  | maINHX2ADD w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]    
   (* _0/1/2: legale se nessun operando/1 byte/1 word *)
   | maIMM1 b ⇒ [ TByte m b ]
+  | maIMM1EXT b ⇒ [ TByte m b ]
   | maIMM2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
   | maDIR1 b ⇒ [ TByte m b ]
   | maDIR2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]