--- a/src/HOL/Main.thy Thu Dec 01 08:28:02 2005 +0100
+++ b/src/HOL/Main.thy Thu Dec 01 15:45:54 2005 +0100
@@ -18,6 +18,11 @@
claset rules into the clause cache; cf.\ theory @{text
Reconstruction}. *}
+declare subset_refl [intro]
+ text {*Ensures that this important theorem is not superseded by the
+ simplifier's "== True" version.*}
setup ResAxioms.clause_setup
+declare subset_refl [rule del]
+ text {*Removed again because it harms blast's performance.*}
end
--- a/src/HOL/Set.thy Thu Dec 01 08:28:02 2005 +0100
+++ b/src/HOL/Set.thy Thu Dec 01 15:45:54 2005 +0100
@@ -524,7 +524,7 @@
lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
by blast
-lemma subset_refl [simp,intro!]: "A \<subseteq> A"
+lemma subset_refl [simp]: "A \<subseteq> A"
by fast
lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"