HomeIsabelle/Phabricator

formal position for spec rule (not significant for equality);

Authored by makarius.