# HG changeset patch
# User wenzelm
# Date 1360177422 -3600
# Node ID ea0cb5ff5ae7a1158587510a8414c92c5ae1e8ad
# Parent  58e2d0cd81aecba444849e48001249fc24dd58e6
documentation for 'print_rules';

diff -r 58e2d0cd81ae -r ea0cb5ff5ae7 src/Doc/IsarRef/Proof.thy
--- a/src/Doc/IsarRef/Proof.thy	Fri Feb 01 22:24:27 2013 +0100
+++ b/src/Doc/IsarRef/Proof.thy	Wed Feb 06 20:03:42 2013 +0100
@@ -690,6 +690,7 @@
   \chref{ch:gen-tools} and \partref{part:hol}).
 
   \begin{matharray}{rcl}
+    @{command_def "print_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\[0.5ex]
     @{method_def "-"} & : & @{text method} \\
     @{method_def "fact"} & : & @{text method} \\
     @{method_def "assumption"} & : & @{text method} \\
@@ -728,6 +729,14 @@
 
   \begin{description}
   
+  \item @{command "print_rules"} prints rules declared via attributes
+  @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute
+  (Pure) dest} of Isabelle/Pure.
+
+  See also the analogous @{command "print_claset"} command for similar
+  rule declarations of the classical reasoner
+  (\secref{sec:classical}).
+
   \item ``@{method "-"}'' (minus) does nothing but insert the forward
   chaining facts as premises into the goal.  Note that command
   @{command_ref "proof"} without any method actually performs a single
@@ -783,7 +792,7 @@
   
   \item @{attribute (Pure) rule}~@{text del} undeclares introduction,
   elimination, or destruct rules.
-  
+
   \item @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some theorem to all
   of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"} in canonical right-to-left
   order, which means that premises stemming from the @{text "a\<^sub>i"}