X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Fstatus.ma;h=1a7b679e8eff8193a1664a3c1cff75f85b42b462;hb=eb4144a401147a44a9620169eb6dafeb8f5a2c17;hp=e630438dc32b6af51855be797ab37a13cd1422ad;hpb=55e5bef77f163b29feeb9ad4e83376c5aa301297;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/freescale/status.ma b/helm/software/matita/contribs/assembly/freescale/status.ma
index e630438dc..1a7b679e8 100644
--- 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)