added cong atts;
authorwenzelm
Fri Mar 31 22:39:06 2000 +0200 (2000-03-31 ago)
changeset 8644c47735e7bd1c
parent 8643 331f0c75e3dc
child 8645 40036a2ab646
added cong atts;
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Fri Mar 31 22:22:23 2000 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Fri Mar 31 22:39:06 2000 +0200
     1.3 @@ -124,11 +124,15 @@
     1.4  fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
     1.5  
     1.6  val cong_add_global = Simplifier.change_global_ss (op addcongs);
     1.7 +val cong_del_global = Simplifier.change_global_ss (op delcongs);
     1.8  val cong_add_local = Simplifier.change_local_ss (op addcongs);
     1.9 +val cong_del_local = Simplifier.change_local_ss (op delcongs);
    1.10  
    1.11  val cong_attrib_setup =
    1.12 -  [Attrib.add_attributes [("cong", (Attrib.no_args cong_add_global, Attrib.no_args cong_add_local),
    1.13 -    "add rules to simpset and claset simultaneously")]];
    1.14 + [Attrib.add_attributes [("cong",
    1.15 +   (Attrib.add_del_args cong_add_global cong_del_global,
    1.16 +    Attrib.add_del_args cong_add_local cong_del_local),
    1.17 +    "declare Simplifier congruence rules")]];
    1.18  
    1.19  
    1.20  val imp_cong = impI RSN