iff_attrib_setup;
authorwenzelm
Thu Aug 26 19:04:19 1999 +0200 (1999-08-26)
changeset 73692d2110cda81e
parent 7368 6b1b6b7c1df0
child 7370 6407a09ac58f
iff_attrib_setup;
src/HOL/HOL.thy
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/HOL.thy	Thu Aug 26 19:02:21 1999 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Aug 26 19:04:19 1999 +0200
     1.3 @@ -188,7 +188,8 @@
     1.4  use "HOL_lemmas.ML"	setup attrib_setup
     1.5  use "cladata.ML"	setup Classical.setup setup clasetup
     1.6  use "blastdata.ML"	setup Blast.setup
     1.7 -use "simpdata.ML"	setup Simplifier.setup setup simpsetup setup Clasimp.setup
     1.8 +use "simpdata.ML"	setup Simplifier.setup setup iff_attrib_setup
     1.9 +			setup simpsetup setup Clasimp.setup
    1.10  
    1.11  
    1.12  end
     2.1 --- a/src/HOL/simpdata.ML	Thu Aug 26 19:02:21 1999 +0200
     2.2 +++ b/src/HOL/simpdata.ML	Thu Aug 26 19:04:19 1999 +0200
     2.3 @@ -82,7 +82,7 @@
     2.4  val iff_add_global = change_global_css (op addIffs);
     2.5  val iff_add_local = change_local_css (op addIffs);
     2.6  
     2.7 -val simpdata_setup =
     2.8 +val iff_attrib_setup =
     2.9    [Attrib.add_attributes [("iff", (Attrib.no_args iff_add_global, Attrib.no_args iff_add_local),
    2.10      "add rules to simpset and claset simultaneously")]];
    2.11