-notation > "'Ex'≪" non associative with precedence 50 for
- @{'excedencerewritel}.
-
-interpretation "exc_rewl" 'excedencerewritel =
- (cic:/matita/excedence/exc_rewl.con _ _ _).
-
-notation > "'Ex'≫" non associative with precedence 50 for
- @{'excedencerewriter}.
-
-interpretation "exc_rewr" 'excedencerewriter =
- (cic:/matita/excedence/exc_rewr.con _ _ _).
-