(*<*) theory Doc_Proofs imports Main begin (*>*) text_raw ‹\part{Proofs ported from HOL4}› (*<*) end (*>*)