added cong atts;
authorwenzelm
Fri Mar 31 22:22:23 2000 +0200 (2000-03-31 ago)
changeset 8643331f0c75e3dc
parent 8642 140883a538c1
child 8644 c47735e7bd1c
added cong atts;
src/FOL/FOL.thy
src/FOL/simpdata.ML
     1.1 --- a/src/FOL/FOL.thy	Fri Mar 31 22:01:01 2000 +0200
     1.2 +++ b/src/FOL/FOL.thy	Fri Mar 31 22:22:23 2000 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  use "cladata.ML"        setup Cla.setup setup clasetup
     1.5  use "blastdata.ML"      setup Blast.setup
     1.6  use "FOL_lemmas2.ML"
     1.7 -use "simpdata.ML"       setup simpsetup
     1.8 +use "simpdata.ML"       setup simpsetup setup cong_attrib_setup
     1.9                          setup "Simplifier.method_setup Splitter.split_modifiers"
    1.10                          setup Splitter.setup setup Clasimp.setup
    1.11  
     2.1 --- a/src/FOL/simpdata.ML	Fri Mar 31 22:01:01 2000 +0200
     2.2 +++ b/src/FOL/simpdata.ML	Fri Mar 31 22:22:23 2000 +0200
     2.3 @@ -304,6 +304,17 @@
     2.4  fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
     2.5  fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
     2.6  
     2.7 +val cong_add_global = Simplifier.change_global_ss (op addcongs);
     2.8 +val cong_del_global = Simplifier.change_global_ss (op delcongs);
     2.9 +val cong_add_local = Simplifier.change_local_ss (op addcongs);
    2.10 +val cong_del_local = Simplifier.change_local_ss (op delcongs);
    2.11 +
    2.12 +val cong_attrib_setup =
    2.13 + [Attrib.add_attributes [("cong",
    2.14 +   (Attrib.add_del_args cong_add_global cong_del_global,
    2.15 +    Attrib.add_del_args cong_add_local cong_del_local),
    2.16 +    "declare Simplifier congruence rules")]];
    2.17 +
    2.18  
    2.19  val meta_simps =
    2.20     [triv_forall_equality,  (* prunes params *)