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