diff -r b794db0b79db -r b1258b7d2789 Prelude.thy --- a/Prelude.thy Fri Jun 03 13:59:21 2011 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,19 +0,0 @@ -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: - "(\x. (x \ A) = (x \ B)) \ A = B" -by blast - - -end \ No newline at end of file