--- a/doc-src/Ref/ref.ind Mon Dec 08 13:56:49 1997 +0100
+++ b/doc-src/Ref/ref.ind Mon Dec 08 13:57:19 1997 +0100
@@ -347,7 +347,7 @@
\item {\tt inst_step_tac}, \bold{130}
\item {\tt instance} section, 53
\item {\tt instantiate}, \bold{46}
- \item {\tt instantiate'}, \bold{39}
+ \item {\tt instantiate'}, \bold{39}, 46
\item instantiation, 18, 39, 46
\item {\tt INTLEAVE}, \bold{29}, 31
\item {\tt INTLEAVE'}, 36
@@ -381,7 +381,7 @@
\item macros, 86--92
\item {\tt make_elim}, \bold{40}, 125
- \item {\tt Match} exception, 93, 99
+ \item {\tt Match} exception, 94, 99
\item {\tt match_tac}, \bold{18}, 124
\item {\tt max_pri}, 66, \bold{72}
\item {\tt merge_ss}, 107
@@ -601,7 +601,7 @@
\item {\tt show_brackets}, \bold{4}
\item {\tt show_consts}, \bold{4}
\item {\tt show_hyps}, \bold{4}
- \item {\tt show_sorts}, \bold{4}, 85
+ \item {\tt show_sorts}, \bold{4}, 85, 93
\item {\tt show_types}, \bold{4}, 85, 88, 95
\item {\tt Sign.sg} ML type, 51
\item {\tt Sign.stamp_names_of}, \bold{59}
@@ -799,6 +799,7 @@
\item type unknowns, \bold{62}, 68
\subitem freezing/thawing of, 46
\item type variables, \bold{62}
+ \item {\tt typed_print_translation}, 93
\item types, \bold{62}
\subitem certified, \bold{62}
\subitem printing of, 4, 15, 62
--- a/doc-src/Ref/ref.tex Mon Dec 08 13:56:49 1997 +0100
+++ b/doc-src/Ref/ref.tex Mon Dec 08 13:57:19 1997 +0100
@@ -1,12 +1,5 @@
\documentclass[12pt]{report}
-\usepackage{a4}
-
-\makeatletter
-\input{../proof.sty}
-\input{../rail.sty}
-\input{../iman.sty}
-\input{../extra.sty}
-\makeatother
+\usepackage{a4,../iman,../extra,../proof,../rail}
%% $Id$
%%\includeonly{}
--- a/doc-src/Ref/thm.tex Mon Dec 08 13:56:49 1997 +0100
+++ b/doc-src/Ref/thm.tex Mon Dec 08 13:57:19 1997 +0100
@@ -132,13 +132,13 @@
\end{ttdescription}
-\subsection{Instantiating a theorem} \label{sec:instantiate}
+\subsection{Instantiating unknowns in a theorem} \label{sec:instantiate}
\index{instantiation}
\begin{ttbox}
-read_instantiate : (string * string) list -> thm -> thm
-read_instantiate_sg : Sign.sg -> (string * string) list -> thm -> thm
-cterm_instantiate : (cterm * cterm) list -> thm -> thm
-instantiate' : ctyp option list -> cterm option list -> thm -> thm
+read_instantiate : (string*string) list -> thm -> thm
+read_instantiate_sg : Sign.sg -> (string*string) list -> thm -> thm
+cterm_instantiate : (cterm*cterm) list -> thm -> thm
+instantiate' : ctyp option list -> cterm option list -> thm -> thm
\end{ttbox}
These meta-rules instantiate type and term unknowns in a theorem. They are
occasionally useful. They can prevent difficulties with higher-order
@@ -223,7 +223,7 @@
prems_of : thm -> term list
cprems_of : thm -> cterm list
nprems_of : thm -> int
-tpairs_of : thm -> (term * term) list
+tpairs_of : thm -> (term*term) list
sign_of_thm : thm -> Sign.sg
theory_of_thm : thm -> theory
dest_state : thm * int -> (term * term) list * term list * term * term