# HG changeset patch
# User wenzelm
# Date 968352964 -7200
# Node ID 5a9081c3b869ab250a1f3f696db1d4b67b256450
# Parent  5f28e5b4c68ee9e5f3c0e7f4e594e1b02ea76750
tuned att names / msgs;

diff -r 5f28e5b4c68e -r 5a9081c3b869 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Sep 07 20:55:18 2000 +0200
+++ b/src/Provers/classical.ML	Thu Sep 07 20:56:04 2000 +0200
@@ -1041,14 +1041,14 @@
 
 (* setup_attrs *)
 
-fun elimify x = Attrib.no_args (Drule.rule_attribute (K make_elim)) x;
+fun elimified x = Attrib.no_args (Drule.rule_attribute (K make_elim)) x;
 
 val setup_attrs = Attrib.add_attributes
- [("elimify", (elimify, elimify), "turn destruct rule into elimination rule (classical)"),
-  (destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declare destruction rule"),
-  (elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "declare elimination rule"),
-  (introN, cla_attr (op addXIs) (op addIs) (op addSIs), "declare introduction rule"),
-  (delruleN, del_attr, "undeclare rule")];
+ [("elimified", (elimified, elimified), "destruct rule turned into elimination rule (classical)"),
+  (destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declaration of destruction rule"),
+  (elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "declaration of elimination rule"),
+  (introN, cla_attr (op addXIs) (op addIs) (op addSIs), "declaration of introduction rule"),
+  (delruleN, del_attr, "remove declaration of elim/intro rule")];
 
 
 
diff -r 5f28e5b4c68e -r 5a9081c3b869 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Thu Sep 07 20:55:18 2000 +0200
+++ b/src/Provers/simplifier.ML	Thu Sep 07 20:56:04 2000 +0200
@@ -463,6 +463,9 @@
 val addN = "add";
 val delN = "del";
 val onlyN = "only";
+val no_asmN = "no_asm";
+val no_asm_useN = "no_asm_use";
+val no_asm_simpN = "no_asm_simp";
 
 val simp_attr =
  (Attrib.add_del_args simp_add_global simp_del_global,
@@ -475,20 +478,31 @@
 
 (* conversions *)
 
-fun conv_attr f =
-  (Attrib.no_args (Drule.rule_attribute (f o simpset_of)),
-    Attrib.no_args (Drule.rule_attribute (f o get_local_simpset)));
+local
+
+fun conv_mode x =
+  ((Args.parens (Args.$$$ no_asmN) >> K simplify ||
+    Args.parens (Args.$$$ no_asm_simpN) >> K asm_simplify ||
+    Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
+    Scan.succeed asm_full_simplify) |> Scan.lift) x;
+
+fun simplified_att get =
+  Attrib.syntax (conv_mode >> (fn f => Drule.rule_attribute (f o get)));
+
+in
+
+val simplified_attr =
+  (simplified_att simpset_of, simplified_att get_local_simpset);
+
+end;
 
 
 (* setup_attrs *)
 
 val setup_attrs = Attrib.add_attributes
- [(simpN,               simp_attr, "declare simplification rule"),
-  (congN,               cong_attr, "declare Simplifier congruence rule"),
-  ("simplify",          conv_attr simplify, "simplify rule"),
-  ("asm_simplify",      conv_attr asm_simplify, "simplify rule, using assumptions"),
-  ("full_simplify",     conv_attr full_simplify, "fully simplify rule"),
-  ("asm_full_simplify", conv_attr asm_full_simplify, "fully simplify rule, using assumptions")];
+ [(simpN, simp_attr, "declaration of simplification rule"),
+  (congN, cong_attr, "declaration of Simplifier congruence rule"),
+  ("simplified", simplified_attr, "simplified rule")];
 
 
 
@@ -497,9 +511,9 @@
 (* simplification *)
 
 val simp_options =
- (Args.parens (Args.$$$ "no_asm") >> K simp_tac ||
-  Args.parens (Args.$$$ "no_asm_simp") >> K asm_simp_tac ||
-  Args.parens (Args.$$$ "no_asm_use") >> K full_simp_tac ||
+ (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
+  Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
+  Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
   Scan.succeed asm_full_simp_tac);
 
 val cong_modifiers =