Snapshot.

[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 e9d374145fce5614e646a758169b5e8f6407be3a..4072f445fa02952d817490c05532ba1d7d0dbe5e 100644 (file)
--- a/helm/software/matita/contribs/assembly/freescale/status.ma
+++ b/helm/software/matita/contribs/assembly/freescale/status.ma
@@ -70,7 +70,7 @@ notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'Sp_Reg'
  non associative with precedence 80 for
  @{ 'mk_alu_HC05 $acclow $indxlow $sp $spm $spf $pc $pcm $hfl $ifl $nfl $zfl $cfl $irqfl }.
 interpretation "mk_alu_HC05" 'mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl =
- (cic:/matita/freescale/status/alu_HC05.ind#xpointer(1/1/1) acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl).
+ (mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl).
  
 (* ALU dell'HC08/HCS08 *) 
 record alu_HC08: Type ≝
@@ -107,7 +107,7 @@ notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'H_Reg'
  non associative with precedence 80 for
  @{ 'mk_alu_HC08 $acclow $indxlow $indxhigh $sp $pc $vfl $hfl $ifl $nfl $zfl $cfl $irqfl }.
 interpretation "mk_alu_HC08" 'mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl =
- (cic:/matita/freescale/status/alu_HC08.ind#xpointer(1/1/1) acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
+ (mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
 
 (* ALU dell'RS08 *)
 record alu_RS08: Type ≝
@@ -149,7 +149,7 @@ notation "{hvbox('A_Reg' ≝ acclow ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' 
  non associative with precedence 80 for
  @{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }.
 interpretation "mk_alu_RS08" 'mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl =
- (cic:/matita/freescale/status/alu_RS08.ind#xpointer(1/1/1) acclow pc pcm spc xm psm zfl cfl).
+ (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl).
 
 (* tipo processore dipendente dalla mcu, varia solo la ALU *)
 record any_status (mcu:mcu_type) (t:memory_impl): Type ≝
@@ -171,7 +171,7 @@ record any_status (mcu:mcu_type) (t:memory_impl): Type ≝
 notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80 
  for @{ 'mk_any_status $alu $mem $chk $clk }.
 interpretation "mk_any_status" 'mk_any_status alu mem chk clk =
- (cic:/matita/freescale/status/any_status.ind#xpointer(1/1/1) alu mem chk clk).
+ (mk_any_status alu mem chk clk).
 
 (* **************** *)
 (* GETTER SPECIFICI *)