--- 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 \\
--- a/doc-src/IsarRef/hol.tex Thu Aug 17 18:58:49 2000 +0200
+++ b/doc-src/IsarRef/hol.tex Thu Aug 17 21:06:04 2000 +0200
@@ -380,7 +380,7 @@
\section{Arithmetic}
-\indexisarmeth{arith}\indexisaratt{arith_split}
+\indexisarmeth{arith}\indexisaratt{arith-split}
\begin{matharray}{rcl}
arith & : & \isarmeth \\
arith_split & : & \isaratt \\