HomeIsabelle/Phabricator

small refinements to partition proofs