# HG changeset patch
# User haftmann
# Date 1237468135 -3600
# Node ID 88c29b3b1fa2be495def403e106ae472676b721b
# Parent  b51811144ed4317faae62e2d2506165065405c92# Parent  140b22f220711d718bcaad4dd330d1404bfd77a9
merged

diff -r b51811144ed4 -r 88c29b3b1fa2 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Mar 19 11:51:49 2009 +0100
+++ b/src/HOL/Set.thy	Thu Mar 19 14:08:55 2009 +0100
@@ -561,19 +561,15 @@
   "'a set"}.
 *}
 
-lemma subsetD [elim]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
+lemma subsetD [elim, intro?]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
   -- {* Rule in Modus Ponens style. *}
   by (unfold mem_def) blast
 
-declare subsetD [intro?] -- FIXME
-
-lemma rev_subsetD: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
+lemma rev_subsetD [intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
   -- {* The same, with reversed premises for use with @{text erule} --
       cf @{text rev_mp}. *}
   by (rule subsetD)
 
-declare rev_subsetD [intro?] -- FIXME
-
 text {*
   \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
 *}
@@ -623,8 +619,6 @@
   -- {* Anti-symmetry of the subset relation. *}
   by (iprover intro: set_ext subsetD)
 
-lemmas equalityI [intro!] = subset_antisym
-
 text {*
   \medskip Equality rules from ZF set theory -- are they appropriate
   here?
@@ -1064,11 +1058,6 @@
 
 lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
 
-lemmas mem_simps =
-  insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
-  mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
-  -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}
-
 (*Would like to add these, but the existing code only searches for the
   outer-level constant, which in this case is just "op :"; we instead need
   to use term-nets to associate patterns with rules.  Also, if a rule fails to
@@ -2489,7 +2478,13 @@
   Sup  ("\<Squnion>_" [900] 900)
 
 
-subsection {* Basic ML bindings *}
+subsection {* Misc theorem and ML bindings *}
+
+lemmas equalityI = subset_antisym
+lemmas mem_simps =
+  insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
+  mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
+  -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}
 
 ML {*
 val Ball_def = @{thm Ball_def}