Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added cong atts;
authorwenzelm
Fri, 31 Mar 2000 22:39:06 +0200
changeset 8644 c47735e7bd1c
parent 8643 331f0c75e3dc
child 8645 40036a2ab646
added cong atts;
src/HOL/simpdata.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle