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+
−