diff -r b794db0b79db -r b1258b7d2789 Attic/Prelude.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/Prelude.thy	Mon Jul 25 13:33:38 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