# HG changeset patch
# User wenzelm
# Date 1002187692 -7200
# Node ID 744399c9dd6a76ead2168e803701ce0b395cfa20
# Parent  37cfa9aad9c0d4579ba7b98bf54149152c0b1f1e
print_induct_rules;

diff -r 37cfa9aad9c0 -r 744399c9dd6a doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Thu Oct 04 11:22:10 2001 +0200
+++ b/doc-src/IsarRef/hol.tex	Thu Oct 04 11:28:12 2001 +0200
@@ -279,6 +279,7 @@
 
 
 \section{Proof by cases and induction}\label{sec:induct-method}
+%FIXME move to generic.tex
 
 \subsection{Proof methods}\label{sec:induct-method-proper}
 
@@ -430,8 +431,9 @@
 
 \subsection{Declaring rules}\label{sec:induct-att}
 
-\indexisaratt{cases}\indexisaratt{induct}
+\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}
 \begin{matharray}{rcl}
+  \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\
   cases & : & \isaratt \\
   induct & : & \isaratt \\
 \end{matharray}