# 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}