--- a/src/HOL/HOL.thy Thu Aug 26 19:02:21 1999 +0200
+++ b/src/HOL/HOL.thy Thu Aug 26 19:04:19 1999 +0200
@@ -188,7 +188,8 @@
use "HOL_lemmas.ML" setup attrib_setup
use "cladata.ML" setup Classical.setup setup clasetup
use "blastdata.ML" setup Blast.setup
-use "simpdata.ML" setup Simplifier.setup setup simpsetup setup Clasimp.setup
+use "simpdata.ML" setup Simplifier.setup setup iff_attrib_setup
+ setup simpsetup setup Clasimp.setup
end
--- a/src/HOL/simpdata.ML Thu Aug 26 19:02:21 1999 +0200
+++ b/src/HOL/simpdata.ML Thu Aug 26 19:04:19 1999 +0200
@@ -82,7 +82,7 @@
val iff_add_global = change_global_css (op addIffs);
val iff_add_local = change_local_css (op addIffs);
-val simpdata_setup =
+val iff_attrib_setup =
[Attrib.add_attributes [("iff", (Attrib.no_args iff_add_global, Attrib.no_args iff_add_local),
"add rules to simpset and claset simultaneously")]];