+(*
+notation < "+ term 90 x term 90 y" non associative with precedence 80 for @{'plus $x $y}.
+notation < "★ term 90 x term 90 y" non associative with precedence 80 for @{'mult $x $y}.
+notation < "= term 90 x term 90 y" non associative with precedence 80 for @{'eq $x $y}.
+notation < "\S term 90 x" non associative with precedence 80 for @{'S $x}.
+notation < "\O" non associative with precedence 80 for @{'O}.
+interpretation "O" 'O = O.
+interpretation "S" 'S x y = (S x y).
+interpretation "mult" 'mult x y = (mult x y).
+interpretation "plus" 'plus x y = (plus x y).
+interpretation "eq" 'eq x y = (eq x y).
+*)
+
+interpretation "+" 'my_plus x y = (plus x y).
+interpretation "*" 'my_mult x y = (mult x y).
+interpretation "=" 'my_eq x y = (eq x y).
+interpretation "S" 'my_S x = (S x).
+interpretation "O" 'my_O = O.
+
+notation "x + y" non associative with precedence 50 for @{'my_plus $x $y}.
+notation "x * y" non associative with precedence 55 for @{'my_mult $x $y}.
+notation "x = y" non associative with precedence 45 for @{'my_eq $x $y}.
+notation > "'S' x" non associative with precedence 40 for @{'my_S $x}.
+notation < "'S' x" non associative with precedence 40 for @{'my_S $x}.
+notation "'O'" non associative with precedence 90 for @{'my_O}.
+