Dedekind sigma completeness for the natural numbers.

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

diff --git a/helm/software/matita/contribs/assembly/freescale/word16.ma b/helm/software/matita/contribs/assembly/freescale/word16.ma
index 98d7703b636db370c1b85225f423986b4c3379d2..c47ff7d5136da098b57822ebb495df675b88ce4f 100644 (file)
--- a/helm/software/matita/contribs/assembly/freescale/word16.ma
+++ b/helm/software/matita/contribs/assembly/freescale/word16.ma
@@ -39,8 +39,7 @@ record word16 : Type ≝
 (* \langle \rangle *)
 notation "〈x:y〉" non associative with precedence 80
  for @{ 'mk_word16 $x $y }.
-interpretation "mk_word16" 'mk_word16 x y = 
- (cic:/matita/freescale/word16/word16.ind#xpointer(1/1/1) x y).
+interpretation "mk_word16" 'mk_word16 x y = (mk_word16 x y).
 
 (* operatore = *)
 definition eq_w16 ≝ λw1,w2.(eq_b8 (w16h w1) (w16h w2)) ⊗ (eq_b8 (w16l w1) (w16l w2)).