# HG changeset patch
# User wenzelm
# Date 965422424 -7200
# Node ID 232b09dba0fe808c343735479e1938b786389f65
# Parent  bf459ea9a523e7156910f0c9f2ff1783447ee2f7
subgoals_tac: fixed spelling;

diff -r bf459ea9a523 -r 232b09dba0fe doc-src/Ref/tactic.tex
--- 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}