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_2
begin
section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
text {*
It is now the time for use to discuss further about the way.
*}
end