Representing "but not" in formal grammar

I just came across the following grammar definition:


CommentChar ::


      SourceCharacter but not LineTerminator

But for discussion, I'll present this similar construct:


Digit ::


       '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9'


Zero ::


       '0'


NonZeroDigit ::


       Digit but not Zero

Is this "but not" construct common in formal grammar specifications? If there a name for it?

I realize that NonZeroDigit could be defined by "manually" expanding the nonterminals and finding the difference -- here that process is as straightforward as it gets. But for more complicated "but not" constructs, I imagine that would be painful and error-prone.

Or, in grammars that support it, is this just considered just a sequence of (a) a negative lookahead (for Zero) combined with (b) the nonterminal for Digit.

For context-free grammars (I guess your question concerns this type of formal grammars), it would be not only painful, but also impossible in general.

Suppose we have an algorithm that provides such "expansion" and yields a new grammar without $\text{but not }$occurrences. Then we can take two arbitrary context-free languages $L, L'$ with start nonterminals $A, A'$ respectively, write down a rule $B \longrightarrow A \text{ but not } A'$, run the algorithm on it, and get a context-free grammar for $L\backslash L'$. It contradicts a well-known fact that difference of two context-free languages can be not context-free.

StackExchange Computer Science Q#122045, answer score: 11