# HG changeset patch
# User wenzelm
# Date 936720531 -7200
# Node ID e70255cb10356f834bc65a16612dd4f10f5fb058
# Parent  08a88d4ebd54c392d90afed2a09a4d6ace1272d3
induct method: rule option;

diff -r 08a88d4ebd54 -r e70255cb1035 doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Tue Sep 07 17:21:44 1999 +0200
+++ b/doc-src/IsarRef/hol.tex	Tue Sep 07 18:08:51 1999 +0200
@@ -158,7 +158,7 @@
 \end{matharray}
 
 The $induct$ method provides a uniform interface to induction over datatypes,
-inductive sets, and recursive functions.  Basically, it is just an interface
+inductive sets, recursive functions etc.  Basically, it is just an interface
 to the $rule$ method applied to appropriate instances of the corresponding
 induction rules.
 
@@ -168,15 +168,18 @@
 
   inst: term term?
   ;
-  kind: ('type' | 'set' | 'function') ':' nameref
+  kind: ('type' | 'set' | 'function' | 'rule') ':' nameref
   ;
 \end{rail}
 
 \begin{descr}
 \item [$induct~insts~kind$] abbreviates method $rule~R$, where $R$ is the
-  induction rule of the type~/ set~/ function specified by $kind$ and
-  instantiated by $insts$.  The latter either consists of pairs $P$ $x$
-  (induction predicate and variable), where $P$ is optional.  If $kind$ is
+  induction rule specified by $kind$ and instantiated by $insts$.  The rule is
+  either that of some type, set, or recursive function (defined via TFL), or
+  given explicitly.
+  
+  The instantiation basically consists of a list of $P$ $x$ (induction
+  predicate and variable) specifications, where $P$ is optional.  If $kind$ is
   omitted, the default is to pick a datatype induction rule according to the
   type of some induction variable, which may not be omitted that case.
 \end{descr}