# HG changeset patch
# User wenzelm
# Date 1751806680 -7200
# Node ID c6b3f0ee0a69220f611db352520b95f5b873c5b9
# Parent  be1fb22d9e2a1355aedeabad30f64c95b199b639
tuned messages;

diff -r be1fb22d9e2a -r c6b3f0ee0a69 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Jul 06 14:53:20 2025 +0200
+++ b/src/Provers/classical.ML	Sun Jul 06 14:58:00 2025 +0200
@@ -904,7 +904,7 @@
     Attrib.setup \<^binding>\<open>intro\<close> (Context_Rules.add safe_intro unsafe_intro Context_Rules.intro_query)
       "declaration of Classical introduction rule" #>
     Attrib.setup \<^binding>\<open>rule\<close> (Scan.lift Args.del >> K rule_del)
-      "remove declaration of intro/elim/dest rule");
+      "remove declaration of Classical intro/elim/dest rule");
 
 
 
diff -r be1fb22d9e2a -r c6b3f0ee0a69 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Sun Jul 06 14:53:20 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Sun Jul 06 14:58:00 2025 +0200
@@ -190,12 +190,12 @@
 
 val _ = Theory.setup
  (Attrib.setup \<^binding>\<open>intro\<close> (add intro_bang intro intro_query)
-    "declaration of introduction rule" #>
+    "declaration of Pure introduction rule" #>
   Attrib.setup \<^binding>\<open>elim\<close> (add elim_bang elim elim_query)
-    "declaration of elimination rule" #>
+    "declaration of Pure elimination rule" #>
   Attrib.setup \<^binding>\<open>dest\<close> (add dest_bang dest dest_query)
-    "declaration of destruction rule" #>
+    "declaration of Pure destruction rule" #>
   Attrib.setup \<^binding>\<open>rule\<close> (Scan.lift Args.del >> K rule_del)
-    "remove declaration of intro/elim/dest rule");
+    "remove declaration of Pure intro/elim/dest rule");
 
 end;