Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
theory Myhill imports Myhill_2beginsection {* Direction @{text "regular language \<Rightarrow>finite partition"} *}text {* It is now the time for use to discuss further about the way. *}end