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