130 conclusion unchanged. This rule underlies \ttindex{rewrite_goals_tac}, but |
130 conclusion unchanged. This rule underlies \ttindex{rewrite_goals_tac}, but |
131 serves little purpose in forward proof. |
131 serves little purpose in forward proof. |
132 \end{ttdescription} |
132 \end{ttdescription} |
133 |
133 |
134 |
134 |
135 \subsection{Instantiating a theorem} \label{sec:instantiate} |
135 \subsection{Instantiating unknowns in a theorem} \label{sec:instantiate} |
136 \index{instantiation} |
136 \index{instantiation} |
137 \begin{ttbox} |
137 \begin{ttbox} |
138 read_instantiate : (string * string) list -> thm -> thm |
138 read_instantiate : (string*string) list -> thm -> thm |
139 read_instantiate_sg : Sign.sg -> (string * string) list -> thm -> thm |
139 read_instantiate_sg : Sign.sg -> (string*string) list -> thm -> thm |
140 cterm_instantiate : (cterm * cterm) list -> thm -> thm |
140 cterm_instantiate : (cterm*cterm) list -> thm -> thm |
141 instantiate' : ctyp option list -> cterm option list -> thm -> thm |
141 instantiate' : ctyp option list -> cterm option list -> thm -> thm |
142 \end{ttbox} |
142 \end{ttbox} |
143 These meta-rules instantiate type and term unknowns in a theorem. They are |
143 These meta-rules instantiate type and term unknowns in a theorem. They are |
144 occasionally useful. They can prevent difficulties with higher-order |
144 occasionally useful. They can prevent difficulties with higher-order |
145 unification, and define specialized versions of rules. |
145 unification, and define specialized versions of rules. |
146 \begin{ttdescription} |
146 \begin{ttdescription} |
221 cprop_of : thm -> cterm |
221 cprop_of : thm -> cterm |
222 concl_of : thm -> term |
222 concl_of : thm -> term |
223 prems_of : thm -> term list |
223 prems_of : thm -> term list |
224 cprems_of : thm -> cterm list |
224 cprems_of : thm -> cterm list |
225 nprems_of : thm -> int |
225 nprems_of : thm -> int |
226 tpairs_of : thm -> (term * term) list |
226 tpairs_of : thm -> (term*term) list |
227 sign_of_thm : thm -> Sign.sg |
227 sign_of_thm : thm -> Sign.sg |
228 theory_of_thm : thm -> theory |
228 theory_of_thm : thm -> theory |
229 dest_state : thm * int -> (term * term) list * term list * term * term |
229 dest_state : thm * int -> (term * term) list * term list * term * term |
230 rep_thm : thm -> {\ttlbrace}sign_ref: Sign.sg_ref, der: deriv, maxidx: int, |
230 rep_thm : thm -> {\ttlbrace}sign_ref: Sign.sg_ref, der: deriv, maxidx: int, |
231 shyps: sort list, hyps: term list, prop: term\ttrbrace |
231 shyps: sort list, hyps: term list, prop: term\ttrbrace |