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 Preludeimports Mainbegin(*To make the theory work under Isabelle 2009 and 2011Isabelle 2009: set_extIsabelle 2011: set_eqI*)lemma set_eq_intro: "(\<And>x. (x \<in> A) = (x \<in> B)) \<Longrightarrow> A = B"by blastend