use Attrib.add_del_args;
authorwenzelm
Fri Mar 31 21:55:27 2000 +0200 (2000-03-31)
changeset 86343f34637cb9c0
parent 8633 427ead639d8a
child 8635 2f699cd7b8d7
use Attrib.add_del_args;
src/HOL/Tools/inductive_package.ML
src/Provers/simplifier.ML
src/Provers/splitter.ML
src/Pure/Isar/calculation.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Mar 31 21:54:50 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Mar 31 21:55:27 2000 +0200
     1.3 @@ -124,7 +124,8 @@
     1.4      else [thm]
     1.5    end;
     1.6  
     1.7 -(* mono add/del *)
     1.8 +
     1.9 +(* attributes *)
    1.10  
    1.11  local
    1.12  
    1.13 @@ -136,24 +137,13 @@
    1.14  fun mk_att f g (x, thm) = (f (g thm) x, thm);
    1.15  
    1.16  in
    1.17 -
    1.18 -val mono_add_global = mk_att map_rules_global add_mono;
    1.19 -val mono_del_global = mk_att map_rules_global del_mono;
    1.20 -
    1.21 +  val mono_add_global = mk_att map_rules_global add_mono;
    1.22 +  val mono_del_global = mk_att map_rules_global del_mono;
    1.23  end;
    1.24  
    1.25 -
    1.26 -(* concrete syntax *)
    1.27 -
    1.28 -val monoN = "mono";
    1.29 -val addN = "add";
    1.30 -val delN = "del";
    1.31 -
    1.32 -fun mono_att add del =
    1.33 -  Attrib.syntax (Scan.lift (Args.$$$ addN >> K add || Args.$$$ delN >> K del || Scan.succeed add));
    1.34 -
    1.35  val mono_attr =
    1.36 -  (mono_att mono_add_global mono_del_global, mono_att Attrib.undef_local_attribute Attrib.undef_local_attribute);
    1.37 + (Attrib.add_del_args mono_add_global mono_del_global,
    1.38 +  Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute);
    1.39  
    1.40  
    1.41  
    1.42 @@ -824,8 +814,9 @@
    1.43  
    1.44  (* setup theory *)
    1.45  
    1.46 -val setup = [InductiveData.init,
    1.47 -             Attrib.add_attributes [(monoN, mono_attr, "monotonicity rule")]];
    1.48 +val setup =
    1.49 + [InductiveData.init,
    1.50 +  Attrib.add_attributes [("mono", mono_attr, "monotonicity rule")]];
    1.51  
    1.52  
    1.53  (* outer syntax *)
     2.1 --- a/src/Provers/simplifier.ML	Fri Mar 31 21:54:50 2000 +0200
     2.2 +++ b/src/Provers/simplifier.ML	Fri Mar 31 21:55:27 2000 +0200
     2.3 @@ -451,15 +451,9 @@
     2.4  val onlyN = "only";
     2.5  val otherN = "other";
     2.6  
     2.7 -fun simp_att change =
     2.8 -  (Args.$$$ addN >> K (op addsimps) ||
     2.9 -    Args.$$$ delN >> K (op delsimps) ||
    2.10 -    Scan.succeed (op addsimps))
    2.11 -  >> change
    2.12 -  |> Scan.lift
    2.13 -  |> Attrib.syntax;
    2.14 -
    2.15 -val simp_attr = (simp_att change_global_ss, simp_att change_local_ss);
    2.16 +val simp_attr =
    2.17 + (Attrib.add_del_args simp_add_global simp_del_global,
    2.18 +  Attrib.add_del_args simp_add_local simp_del_local);
    2.19  
    2.20  
    2.21  (* conversions *)
     3.1 --- a/src/Provers/splitter.ML	Fri Mar 31 21:54:50 2000 +0200
     3.2 +++ b/src/Provers/splitter.ML	Fri Mar 31 21:55:27 2000 +0200
     3.3 @@ -398,33 +398,26 @@
     3.4  (* attributes *)
     3.5  
     3.6  val splitN = "split";
     3.7 -val addN = "add";
     3.8 -val delN = "del";
     3.9 -
    3.10 -fun split_att change =
    3.11 -  (Args.$$$ addN >> K (op addsplits) ||
    3.12 -    Args.$$$ delN >> K (op delsplits) ||
    3.13 -    Scan.succeed (op addsplits))
    3.14 -  >> change
    3.15 -  |> Scan.lift
    3.16 -  |> Attrib.syntax;
    3.17 -
    3.18 -val setup_attrs = Attrib.add_attributes
    3.19 - [(splitN, (split_att Simplifier.change_global_ss, split_att Simplifier.change_local_ss),
    3.20 -    "declare splitter rule")];
    3.21  
    3.22  val split_add_global = Simplifier.change_global_ss (op addsplits);
    3.23  val split_del_global = Simplifier.change_global_ss (op delsplits);
    3.24  val split_add_local = Simplifier.change_local_ss (op addsplits);
    3.25  val split_del_local = Simplifier.change_local_ss (op delsplits);
    3.26  
    3.27 +val split_attr =
    3.28 + (Attrib.add_del_args split_add_global split_del_global,
    3.29 +  Attrib.add_del_args split_add_local split_del_local);
    3.30 +
    3.31 +val setup_attrs =
    3.32 +  Attrib.add_attributes [(splitN, split_attr, "declare splitter rule")];
    3.33 +
    3.34  
    3.35  (* method modifiers *)
    3.36  
    3.37  val split_modifiers =
    3.38   [Args.$$$ splitN -- Args.$$$ ":" >> K ((I, split_add_local): Method.modifier),
    3.39 -  Args.$$$ splitN -- Args.$$$ addN -- Args.$$$ ":" >> K (I, split_add_local),
    3.40 -  Args.$$$ splitN -- Args.$$$ delN -- Args.$$$ ":" >> K (I, split_del_local)];
    3.41 +  Args.$$$ splitN -- Args.$$$ "add" -- Args.$$$ ":" >> K (I, split_add_local),
    3.42 +  Args.$$$ splitN -- Args.$$$ "del" -- Args.$$$ ":" >> K (I, split_del_local)];
    3.43  
    3.44  
    3.45  
     4.1 --- a/src/Pure/Isar/calculation.ML	Fri Mar 31 21:54:50 2000 +0200
     4.2 +++ b/src/Pure/Isar/calculation.ML	Fri Mar 31 21:55:27 2000 +0200
     4.3 @@ -91,15 +91,9 @@
     4.4  
     4.5  (* concrete syntax *)
     4.6  
     4.7 -val transN = "trans";
     4.8 -val addN = "add";
     4.9 -val delN = "del";
    4.10 -
    4.11 -fun trans_att add del =
    4.12 -  Attrib.syntax (Scan.lift (Args.$$$ addN >> K add || Args.$$$ delN >> K del || Scan.succeed add));
    4.13 -
    4.14  val trans_attr =
    4.15 -  (trans_att trans_add_global trans_del_global, trans_att trans_add_local trans_del_local);
    4.16 + (Attrib.add_del_args trans_add_global trans_del_global,
    4.17 +  Attrib.add_del_args trans_add_local trans_del_local);
    4.18  
    4.19  
    4.20  
    4.21 @@ -181,7 +175,7 @@
    4.22  (** theory setup **)
    4.23  
    4.24  val setup = [GlobalCalculation.init, LocalCalculation.init,
    4.25 -  Attrib.add_attributes [(transN, trans_attr, "declare transitivity rule")]];
    4.26 +  Attrib.add_attributes [("trans", trans_attr, "declare transitivity rule")]];
    4.27  
    4.28  
    4.29  end;