--- a/Prelude.thy	Fri Jun 03 13:59:21 2011 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-theory Prelude
-imports Main
-begin
-
-(*
-To make the theory work under Isabelle 2009 and 2011
-
-Isabelle 2009: set_ext
-Isabelle 2011: set_eqI
-
-*)
-
-
-lemma set_eq_intro:
-  "(\<And>x. (x \<in> A) = (x \<in> B)) \<Longrightarrow> A = B"
-by blast
-
-
-end
\ No newline at end of file