HomeIsabelle/Phabricator

new theorem has_integral_UN