--- a/src/HOL/Set.thy Wed Mar 18 15:23:52 2009 +0100
+++ b/src/HOL/Set.thy Thu Mar 19 14:08:41 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}