--- a/doc-src/IsarRef/generic.tex Thu Aug 17 18:58:49 2000 +0200
+++ b/doc-src/IsarRef/generic.tex Thu Aug 17 21:06:04 2000 +0200
@@ -396,7 +396,7 @@
\indexisarmeth{rule-tac}\indexisarmeth{erule-tac}
\indexisarmeth{drule-tac}\indexisarmeth{frule-tac}
\indexisarmeth{cut-tac}\indexisarmeth{thin-tac}
-\indexisarmeth{subgoal-tac}\indexisarmeth{rename_tac}
+\indexisarmeth{subgoal-tac}\indexisarmeth{rename-tac}
\indexisarmeth{rotate-tac}\indexisarmeth{tactic}
\begin{matharray}{rcl}
rule_tac^* & : & \isarmeth \\