HomeIsabelle/Phabricator

proper theory for export_proofs;