# 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} \\