1
theory Prelude
2
imports Main
3
begin
4
5
(*
6
To make the theory work under Isabelle 2009 and 2011
7
8
Isabelle 2009: set_ext
9
Isabelle 2011: set_eqI
10
11
*)
12
13
14
lemma set_eq_intro:
15
"(\<And>x. (x \<in> A) = (x \<in> B)) \<Longrightarrow> A = B"
16
by blast
17
18
19
end