X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fassembly%2Fbyte.ma;h=8c7be030844377c961ad25c81d555fdedf33fe9d;hb=9a3b49d3584873c77a39107cb5ee4f1e6010e43c;hp=4d050e0cda93fadd1d08b10b07b5268cbde01e48;hpb=d27cfdc825df15aade7edd457b08ee614d44aa32;p=helm.git

diff --git a/helm/software/matita/library/assembly/byte.ma b/helm/software/matita/library/assembly/byte.ma
index 4d050e0cd..8c7be0308 100644
--- a/helm/software/matita/library/assembly/byte.ma
+++ b/helm/software/matita/library/assembly/byte.ma
@@ -14,13 +14,17 @@
 
 set "baseuri" "cic:/matita/assembly/byte".
 
-include "exadecimal.ma".
+include "assembly/exadecimal.ma".
 
 record byte : Type ≝ {
  bh: exadecimal;
  bl: exadecimal
 }.
 
+notation "〈 x, y 〉" non associative with precedence 80 for @{ 'mk_byte $x $y }.
+interpretation "mk_byte" 'mk_byte x y = 
+ (cic:/matita/assembly/byte/byte.ind#xpointer(1/1/1) x y).
+
 definition eqbyte ≝
  λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
 
@@ -205,7 +209,7 @@ qed.
 
 
 lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
- ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b)) = false.
+ ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b))) = false.
  intros;
  unfold byte_of_nat;
  cut (b < 15 ∨ b ≥ 15);