--- a/doc-src/IsarRef/logics.tex Thu Apr 24 11:38:10 2008 +0200
+++ b/doc-src/IsarRef/logics.tex Thu Apr 24 11:38:42 2008 +0200
@@ -535,9 +535,9 @@
\subsubsection{Proof methods related to recursive definitions}
-\indexisarmethof{HOL}{pat\_completeness}
+\indexisarmethof{HOL}{pat-completeness}
\indexisarmethof{HOL}{relation}
-\indexisarmethof{HOL}{lexicographic\_order}
+\indexisarmethof{HOL}{lexicographic-order}
\begin{matharray}{rcl}
pat\_completeness & : & \isarmeth \\
@@ -1188,7 +1188,7 @@
method assists users in this task; a version of this is already declared as a
``solver'' in the standard Simplifier setup.
-\indexisarcmd{print-tcset}\indexisaratt{typecheck}\indexisaratt{TC}
+\indexisarcmdof{ZF}{print-tcset}\indexisarattof{ZF}{typecheck}\indexisarattof{ZF}{TC}
\begin{matharray}{rcl}
\isarcmd{print_tcset}^* & : & \isarkeep{theory~|~proof} \\