print_induct_rules;
authorwenzelm
Thu Oct 04 11:28:12 2001 +0200 (2001-10-04)
changeset 11662744399c9dd6a
parent 11661 37cfa9aad9c0
child 11663 8a86409108fe
print_induct_rules;
doc-src/IsarRef/hol.tex
     1.1 --- a/doc-src/IsarRef/hol.tex	Thu Oct 04 11:22:10 2001 +0200
     1.2 +++ b/doc-src/IsarRef/hol.tex	Thu Oct 04 11:28:12 2001 +0200
     1.3 @@ -279,6 +279,7 @@
     1.4  
     1.5  
     1.6  \section{Proof by cases and induction}\label{sec:induct-method}
     1.7 +%FIXME move to generic.tex
     1.8  
     1.9  \subsection{Proof methods}\label{sec:induct-method-proper}
    1.10  
    1.11 @@ -430,8 +431,9 @@
    1.12  
    1.13  \subsection{Declaring rules}\label{sec:induct-att}
    1.14  
    1.15 -\indexisaratt{cases}\indexisaratt{induct}
    1.16 +\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}
    1.17  \begin{matharray}{rcl}
    1.18 +  \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\
    1.19    cases & : & \isaratt \\
    1.20    induct & : & \isaratt \\
    1.21  \end{matharray}