freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / assembly / freescale / status.ma

diff --git a/helm/software/matita/contribs/assembly/freescale/status.ma b/helm/software/matita/contribs/assembly/freescale/status.ma
index e630438dc32b6af51855be797ab37a13cd1422ad..1a7b679e8eff8193a1664a3c1cff75f85b42b462 100644 (file)
--- a/helm/software/matita/contribs/assembly/freescale/status.ma
+++ b/helm/software/matita/contribs/assembly/freescale/status.ma
@@ -607,7 +607,7 @@ definition set_sp_reg_HC05 ≝
 λalu.λsp':word16.
  mk_alu_HC05
   (acc_low_reg_HC05 alu)
-  (indx_low_reg_HC05 alu)
+  (indX_low_reg_HC05 alu)
   (or_w16 (and_w16 sp' (sp_mask_HC05 alu)) (sp_fix_HC05 alu))
   (sp_mask_HC05 alu)
   (sp_fix_HC05 alu)
@@ -660,7 +660,7 @@ definition set_pc_reg_HC05 ≝
 λalu.λpc':word16.
  mk_alu_HC05
   (acc_low_reg_HC05 alu)
-  (indx_low_reg_HC05 alu)
+  (indX_low_reg_HC05 alu)
   (sp_reg_HC05 alu)
   (sp_mask_HC05 alu)
   (sp_fix_HC05 alu)
@@ -849,7 +849,7 @@ definition set_h_flag_HC05 ≝
 λalu.λhfl':bool.
  mk_alu_HC05
   (acc_low_reg_HC05 alu)
-  (indx_low_reg_HC05 alu)
+  (indX_low_reg_HC05 alu)
   (sp_reg_HC05 alu)
   (sp_mask_HC05 alu)
   (sp_fix_HC05 alu)
@@ -902,7 +902,7 @@ definition set_i_flag_HC05 ≝
 λalu.λifl':bool.
  mk_alu_HC05
   (acc_low_reg_HC05 alu)
-  (indx_low_reg_HC05 alu)
+  (indX_low_reg_HC05 alu)
   (sp_reg_HC05 alu)
   (sp_mask_HC05 alu)
   (sp_fix_HC05 alu)
@@ -955,7 +955,7 @@ definition set_n_flag_HC05 ≝
 λalu.λnfl':bool.
  mk_alu_HC05
   (acc_low_reg_HC05 alu)
-  (indx_low_reg_HC05 alu)
+  (indX_low_reg_HC05 alu)
   (sp_reg_HC05 alu)
   (sp_mask_HC05 alu)
   (sp_fix_HC05 alu)
@@ -1008,7 +1008,7 @@ definition set_z_flag_HC05 ≝
 λalu.λzfl':bool.
  mk_alu_HC05
   (acc_low_reg_HC05 alu)
-  (indx_low_reg_HC05 alu)
+  (indX_low_reg_HC05 alu)
   (sp_reg_HC05 alu)
   (sp_mask_HC05 alu)
   (sp_fix_HC05 alu)
@@ -1069,7 +1069,7 @@ definition set_c_flag_HC05 ≝
 λalu.λcfl':bool.
  mk_alu_HC05
   (acc_low_reg_HC05 alu)
-  (indx_low_reg_HC05 alu)
+  (indX_low_reg_HC05 alu)
   (sp_reg_HC05 alu)
   (sp_mask_HC05 alu)
   (sp_fix_HC05 alu)
@@ -1130,7 +1130,7 @@ definition set_irq_flag_HC05 ≝
 λalu.λirqfl':bool.
  mk_alu_HC05
   (acc_low_reg_HC05 alu)
-  (indx_low_reg_HC05 alu)
+  (indX_low_reg_HC05 alu)
   (sp_reg_HC05 alu)
   (sp_mask_HC05 alu)
   (sp_fix_HC05 alu)