Dedekind sigma completeness for the natural numbers.

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

diff --git a/helm/software/matita/contribs/assembly/freescale/byte8.ma b/helm/software/matita/contribs/assembly/freescale/byte8.ma
index f3d2e10b441b23145c97bbcc38316f291664bb84..6f1c484048ae6382d11961441ec7c286579a0b4e 100644 (file)
--- a/helm/software/matita/contribs/assembly/freescale/byte8.ma
+++ b/helm/software/matita/contribs/assembly/freescale/byte8.ma
@@ -39,8 +39,7 @@ record byte8 : Type ≝
 (* \langle \rangle *)
 notation "〈x,y〉" non associative with precedence 80
  for @{ 'mk_byte8 $x $y }.
-interpretation "mk_byte8" 'mk_byte8 x y = 
- (cic:/matita/freescale/byte8/byte8.ind#xpointer(1/1/1) x y).
+interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y).
 
 (* operatore = *)
 definition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1) (b8l b2)).