--- a/src/HOL/simpdata.ML Fri Mar 31 22:22:23 2000 +0200
+++ b/src/HOL/simpdata.ML Fri Mar 31 22:39:06 2000 +0200
@@ -124,11 +124,15 @@
fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
val cong_add_global = Simplifier.change_global_ss (op addcongs);
+val cong_del_global = Simplifier.change_global_ss (op delcongs);
val cong_add_local = Simplifier.change_local_ss (op addcongs);
+val cong_del_local = Simplifier.change_local_ss (op delcongs);
val cong_attrib_setup =
- [Attrib.add_attributes [("cong", (Attrib.no_args cong_add_global, Attrib.no_args cong_add_local),
- "add rules to simpset and claset simultaneously")]];
+ [Attrib.add_attributes [("cong",
+ (Attrib.add_del_args cong_add_global cong_del_global,
+ Attrib.add_del_args cong_add_local cong_del_local),
+ "declare Simplifier congruence rules")]];
val imp_cong = impI RSN