+notation "hvbox(m break {a ↦ break v})" non associative with precedence 80 for
+ @{ 'update $m $a $v }.
+
+notation "hvbox(m break {a ↦ break v} \nbsp x)" non associative with precedence 80 for
+ @{ 'update4 $m $a $v $x }.
+
+interpretation "update" 'update m a v =
+ (cic:/matita/assembly/vm/update.con m a v).
+
+interpretation "update4" 'update4 m a v x =
+ (cic:/matita/assembly/vm/update.con m a v x).
+