--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Mon Mar 16 19:40:03 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Mon Mar 16 23:36:55 2009 +0100
@@ -821,12 +821,12 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{MetaSimplifier.norm\_hhf}\verb|MetaSimplifier.norm_hhf: thm -> thm| \\
+ \indexdef{}{ML}{Simplifier.norm\_hhf}\verb|Simplifier.norm_hhf: thm -> thm| \\
\end{mldecls}
\begin{description}
- \item \verb|MetaSimplifier.norm_hhf|~\isa{thm} normalizes the given
+ \item \verb|Simplifier.norm_hhf|~\isa{thm} normalizes the given
theorem according to the canonical form specified above. This is
occasionally helpful to repair some low-level tools that do not
handle Hereditary Harrop Formulae properly.