HomeIsabelle/Phabricator

A few new theorems, plus some tidying up