(* \ominus *)
notation "hvbox(⊖ a)" non associative with precedence 36
for @{ 'not_bool $a }.
-interpretation "not_bool" 'not_bool x =
- (cic:/matita/freescale/extra/not_bool.con x).
+interpretation "not_bool" 'not_bool x = (not_bool x).
(* \otimes *)
notation "hvbox(a break ⊗ b)" left associative with precedence 35
for @{ 'and_bool $a $b }.
-interpretation "and_bool" 'and_bool x y =
- (cic:/matita/freescale/extra/and_bool.con x y).
+interpretation "and_bool" 'and_bool x y = (and_bool x y).
(* \oplus *)
notation "hvbox(a break ⊕ b)" left associative with precedence 34
for @{ 'or_bool $a $b }.
-interpretation "or_bool" 'or_bool x y =
- (cic:/matita/freescale/extra/or_bool.con x y).
+interpretation "or_bool" 'or_bool x y = (or_bool x y).
(* \odot *)
notation "hvbox(a break ⊙ b)" left associative with precedence 33
for @{ 'xor_bool $a $b }.
-interpretation "xor_bool" 'xor_bool x y =
- (cic:/matita/freescale/extra/xor_bool.con x y).
+interpretation "xor_bool" 'xor_bool x y = (xor_bool x y).
(* ProdT e' gia' definito, aggiungo Prod3T e Prod4T e Prod5T *)