(*<*) theory Paper imports "../Myhill" begin (*>*) section {* Introduction *} text {* *} (*<*) end (*>*)