Prelude.thy
author urbanc
Tue, 19 Apr 2011 02:19:56 +0000 (2011-04-19)
changeset 154 7c68b9ad4486
parent 35 d2ddce8b36fd
permissions -rw-r--r--
implemented most suggestions from the reviewers
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