diff -r 751d800fddf2 -r d2ddce8b36fd Prelude.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Prelude.thy	Wed Jan 26 22:23:56 2011 +0000
@@ -0,0 +1,19 @@
+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