equal
deleted
inserted
replaced
242 \index{tactics!for inserting facts}\index{assumptions!inserting} |
242 \index{tactics!for inserting facts}\index{assumptions!inserting} |
243 \begin{ttbox} |
243 \begin{ttbox} |
244 cut_facts_tac : thm list -> int -> tactic |
244 cut_facts_tac : thm list -> int -> tactic |
245 cut_inst_tac : (string*string)list -> thm -> int -> tactic |
245 cut_inst_tac : (string*string)list -> thm -> int -> tactic |
246 subgoal_tac : string -> int -> tactic |
246 subgoal_tac : string -> int -> tactic |
|
247 subgoal_tacs : string list -> int -> tactic |
247 \end{ttbox} |
248 \end{ttbox} |
248 These tactics add assumptions to a given subgoal. |
249 These tactics add assumptions to a given subgoal. |
249 \begin{ttdescription} |
250 \begin{ttdescription} |
250 \item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] |
251 \item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] |
251 adds the {\it thms} as new assumptions to subgoal~$i$. Once they have |
252 adds the {\it thms} as new assumptions to subgoal~$i$. Once they have |
262 new assumption to subgoal~$i$. |
263 new assumption to subgoal~$i$. |
263 |
264 |
264 \item[\ttindexbold{subgoal_tac} {\it formula} {\it i}] |
265 \item[\ttindexbold{subgoal_tac} {\it formula} {\it i}] |
265 adds the {\it formula} as a assumption to subgoal~$i$, and inserts the same |
266 adds the {\it formula} as a assumption to subgoal~$i$, and inserts the same |
266 {\it formula} as a new subgoal, $i+1$. |
267 {\it formula} as a new subgoal, $i+1$. |
|
268 |
|
269 \item[\ttindexbold{subgoals_tac} {\it formulae} {\it i}] |
|
270 uses {\tt subgoal_tac} to add the members of the list of {\it |
|
271 formulae} as assumptions to subgoal~$i$. |
267 \end{ttdescription} |
272 \end{ttdescription} |
268 |
273 |
269 |
274 |
270 \subsection{Theorems useful with tactics} |
275 \subsection{Theorems useful with tactics} |
271 \index{theorems!of pure theory} |
276 \index{theorems!of pure theory} |