author | wenzelm |
Fri, 04 Aug 2000 22:53:44 +0200 | |
changeset 9523 | 232b09dba0fe |
parent 9522 | bf459ea9a523 |
child 9524 | 5721615da108 |
--- a/doc-src/Ref/tactic.tex Fri Aug 04 11:47:28 2000 +0200 +++ b/doc-src/Ref/tactic.tex Fri Aug 04 22:53:44 2000 +0200 @@ -229,7 +229,7 @@ cut_facts_tac : thm list -> int -> tactic cut_inst_tac : (string*string)list -> thm -> int -> tactic subgoal_tac : string -> int -> tactic -subgoal_tacs : string list -> int -> tactic +subgoals_tac : string list -> int -> tactic \end{ttbox} These tactics add assumptions to a subgoal. \begin{ttdescription}