(*<*) theory Proof_Object imports Formula Partition Regex_Proof_Object begin (*>*) section ‹Proof Objects›