src/FOL/simpdata.ML
changeset 8643 331f0c75e3dc
parent 8472 50a653f8b8ea
child 9300 ee5c9672d208
--- a/src/FOL/simpdata.ML	Fri Mar 31 22:01:01 2000 +0200
+++ b/src/FOL/simpdata.ML	Fri Mar 31 22:22:23 2000 +0200
@@ -304,6 +304,17 @@
 fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
 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.add_del_args cong_add_global cong_del_global,
+    Attrib.add_del_args cong_add_local cong_del_local),
+    "declare Simplifier congruence rules")]];
+
 
 val meta_simps =
    [triv_forall_equality,  (* prunes params *)