HomeIsabelle/Phabricator

explicit type class for discrete linordered semidoms