|
35
|
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 |