# HG changeset patch
# User paulson
# Date 1133448354 -3600
# Node ID e52f867ab8516bf8d5fbdfaadab0c2cf340e5fc2
# Parent  4595eb4627fa9f6037461833de3e2026c7763843
restoring the old status of subset_refl

diff -r 4595eb4627fa -r e52f867ab851 src/HOL/Main.thy
--- 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
diff -r 4595eb4627fa -r e52f867ab851 src/HOL/Set.thy
--- 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"