# HG changeset patch
# User wenzelm
# Date 1209029922 -7200
# Node ID b010007e9d31c63fc75dad9356377599c9422348
# Parent  93f36f5f4a3577cd01121aa2eb82b71b1e707086
tuned index commands;

diff -r 93f36f5f4a35 -r b010007e9d31 doc-src/IsarRef/logics.tex
--- 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} \\