tuned att names / msgs;
authorwenzelm
Thu Sep 07 20:56:04 2000 +0200 (2000-09-07 ago)
changeset 98995a9081c3b869
parent 9898 5f28e5b4c68e
child 9900 8035a13c61a0
tuned att names / msgs;
src/Provers/classical.ML
src/Provers/simplifier.ML
     1.1 --- a/src/Provers/classical.ML	Thu Sep 07 20:55:18 2000 +0200
     1.2 +++ b/src/Provers/classical.ML	Thu Sep 07 20:56:04 2000 +0200
     1.3 @@ -1041,14 +1041,14 @@
     1.4  
     1.5  (* setup_attrs *)
     1.6  
     1.7 -fun elimify x = Attrib.no_args (Drule.rule_attribute (K make_elim)) x;
     1.8 +fun elimified x = Attrib.no_args (Drule.rule_attribute (K make_elim)) x;
     1.9  
    1.10  val setup_attrs = Attrib.add_attributes
    1.11 - [("elimify", (elimify, elimify), "turn destruct rule into elimination rule (classical)"),
    1.12 -  (destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declare destruction rule"),
    1.13 -  (elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "declare elimination rule"),
    1.14 -  (introN, cla_attr (op addXIs) (op addIs) (op addSIs), "declare introduction rule"),
    1.15 -  (delruleN, del_attr, "undeclare rule")];
    1.16 + [("elimified", (elimified, elimified), "destruct rule turned into elimination rule (classical)"),
    1.17 +  (destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declaration of destruction rule"),
    1.18 +  (elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "declaration of elimination rule"),
    1.19 +  (introN, cla_attr (op addXIs) (op addIs) (op addSIs), "declaration of introduction rule"),
    1.20 +  (delruleN, del_attr, "remove declaration of elim/intro rule")];
    1.21  
    1.22  
    1.23  
     2.1 --- a/src/Provers/simplifier.ML	Thu Sep 07 20:55:18 2000 +0200
     2.2 +++ b/src/Provers/simplifier.ML	Thu Sep 07 20:56:04 2000 +0200
     2.3 @@ -463,6 +463,9 @@
     2.4  val addN = "add";
     2.5  val delN = "del";
     2.6  val onlyN = "only";
     2.7 +val no_asmN = "no_asm";
     2.8 +val no_asm_useN = "no_asm_use";
     2.9 +val no_asm_simpN = "no_asm_simp";
    2.10  
    2.11  val simp_attr =
    2.12   (Attrib.add_del_args simp_add_global simp_del_global,
    2.13 @@ -475,20 +478,31 @@
    2.14  
    2.15  (* conversions *)
    2.16  
    2.17 -fun conv_attr f =
    2.18 -  (Attrib.no_args (Drule.rule_attribute (f o simpset_of)),
    2.19 -    Attrib.no_args (Drule.rule_attribute (f o get_local_simpset)));
    2.20 +local
    2.21 +
    2.22 +fun conv_mode x =
    2.23 +  ((Args.parens (Args.$$$ no_asmN) >> K simplify ||
    2.24 +    Args.parens (Args.$$$ no_asm_simpN) >> K asm_simplify ||
    2.25 +    Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
    2.26 +    Scan.succeed asm_full_simplify) |> Scan.lift) x;
    2.27 +
    2.28 +fun simplified_att get =
    2.29 +  Attrib.syntax (conv_mode >> (fn f => Drule.rule_attribute (f o get)));
    2.30 +
    2.31 +in
    2.32 +
    2.33 +val simplified_attr =
    2.34 +  (simplified_att simpset_of, simplified_att get_local_simpset);
    2.35 +
    2.36 +end;
    2.37  
    2.38  
    2.39  (* setup_attrs *)
    2.40  
    2.41  val setup_attrs = Attrib.add_attributes
    2.42 - [(simpN,               simp_attr, "declare simplification rule"),
    2.43 -  (congN,               cong_attr, "declare Simplifier congruence rule"),
    2.44 -  ("simplify",          conv_attr simplify, "simplify rule"),
    2.45 -  ("asm_simplify",      conv_attr asm_simplify, "simplify rule, using assumptions"),
    2.46 -  ("full_simplify",     conv_attr full_simplify, "fully simplify rule"),
    2.47 -  ("asm_full_simplify", conv_attr asm_full_simplify, "fully simplify rule, using assumptions")];
    2.48 + [(simpN, simp_attr, "declaration of simplification rule"),
    2.49 +  (congN, cong_attr, "declaration of Simplifier congruence rule"),
    2.50 +  ("simplified", simplified_attr, "simplified rule")];
    2.51  
    2.52  
    2.53  
    2.54 @@ -497,9 +511,9 @@
    2.55  (* simplification *)
    2.56  
    2.57  val simp_options =
    2.58 - (Args.parens (Args.$$$ "no_asm") >> K simp_tac ||
    2.59 -  Args.parens (Args.$$$ "no_asm_simp") >> K asm_simp_tac ||
    2.60 -  Args.parens (Args.$$$ "no_asm_use") >> K full_simp_tac ||
    2.61 + (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
    2.62 +  Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
    2.63 +  Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
    2.64    Scan.succeed asm_full_simp_tac);
    2.65  
    2.66  val cong_modifiers =