summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Tue, 18 Jan 2000 11:00:10 +0100 | |

changeset 8135 | ad1c4a678196 |

parent 8134 | ceedd1a8bad6 |

child 8136 | 8c65f3ca13f2 |

Documented Thm.instantiate (not normalizing) and Drule.instantiate
(normalizing)

--- a/doc-src/Ref/thm.tex Mon Jan 17 15:56:58 2000 +0100 +++ b/doc-src/Ref/thm.tex Tue Jan 18 11:00:10 2000 +0100 @@ -604,24 +604,32 @@ applies {\tt forall_elim_var} repeatedly, for every element of the list~$ks$. \end{ttdescription} + \subsection{Instantiation of unknowns} \index{instantiation} \begin{ttbox} instantiate: (indexname * ctyp){\thinspace}list * (cterm * cterm){\thinspace}list -> thm -> thm \end{ttbox} +There are two versions of this rule. The primitive one is +\ttindexbold{Thm.instantiate}, which merely performs the instantiation and can +produce a conclusion not in normal form. A derived version is +\ttindexbold{Drule.instantiate}, which normalizes its conclusion. + \begin{ttdescription} \item[\ttindexbold{instantiate} ($tyinsts$, $insts$) $thm$] simultaneously substitutes types for type unknowns (the $tyinsts$) and terms for term unknowns (the $insts$). Instantiations are given as $(v,t)$ pairs, where $v$ is an unknown and $t$ is a term (of the same type as $v$) or a type (of the same sort as~$v$). All the unknowns -must be distinct. The rule normalizes its conclusion. +must be distinct. -Note that \ttindex{instantiate'} (see \S\ref{sec:instantiate}) +In some cases, \ttindex{instantiate'} (see \S\ref{sec:instantiate}) provides a more convenient interface to this rule. \end{ttdescription} + + \subsection{Freezing/thawing type unknowns} \index{type unknowns!freezing/thawing of} \begin{ttbox}