# HG changeset patch
# User urbanc
# Date 1296080636 0
# Node ID d2ddce8b36fdc8d88f96713b9ef0393cf433f973
# Parent  751d800fddf2707c5f589fd73ea07f40f4acc901
made the theory work under both Isabelle 2009 and 2011

diff -r 751d800fddf2 -r d2ddce8b36fd Myhill.thy
--- a/Myhill.thy	Wed Jan 26 14:13:18 2011 +0000
+++ b/Myhill.thy	Wed Jan 26 22:23:56 2011 +0000
@@ -1,5 +1,5 @@
 theory Myhill
-  imports Main List_Prefix Prefix_subtract
+  imports Main List_Prefix Prefix_subtract Prelude
 begin
 
 (*
@@ -192,7 +192,7 @@
   *}
 lemma folds_alt_simp [simp]:
   "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)"
-apply (rule set_ext, simp add:folds_def)
+apply (rule set_eq_intro, simp add:folds_def)
 apply (rule someI2_ex, erule finite_imp_fold_graph)
 by (erule fold_graph.induct, auto)
 
diff -r 751d800fddf2 -r d2ddce8b36fd Prelude.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Prelude.thy	Wed Jan 26 22:23:56 2011 +0000
@@ -0,0 +1,19 @@
+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
\ No newline at end of file