+notation > "'Ex'≪" non associative with precedence 50 for
+ @{'excessrewritel}.
+
+interpretation "exc_rewl" 'excessrewritel =
+ (cic:/matita/excess/exc_rewl.con _ _ _).
+
+notation > "'Ex'≫" non associative with precedence 50 for
+ @{'excessrewriter}.
+
+interpretation "exc_rewr" 'excessrewriter =
+ (cic:/matita/excess/exc_rewr.con _ _ _).
+