author wenzelm Tue, 07 Sep 1999 18:08:51 +0200 changeset 7507 e70255cb1035 parent 7506 08a88d4ebd54 child 7508 c8b5dcacf2e3
induct method: rule option;
 doc-src/IsarRef/hol.tex file | annotate | diff | comparison | revisions
--- 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}