--- a/doc-src/IsarImplementation/Thy/document/proof.tex Thu May 08 22:17:37 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex Thu May 08 22:20:33 2008 +0200
@@ -104,15 +104,15 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexml{Variable.add-fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
+ \indexml{Variable.add\_fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
\verb| string list -> Proof.context -> string list * Proof.context| \\
- \indexml{Variable.variant-fixes}\verb|Variable.variant_fixes: |\isasep\isanewline%
+ \indexml{Variable.variant\_fixes}\verb|Variable.variant_fixes: |\isasep\isanewline%
\verb| string list -> Proof.context -> string list * Proof.context| \\
- \indexml{Variable.declare-term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
- \indexml{Variable.declare-constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
+ \indexml{Variable.declare\_term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
+ \indexml{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
\indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
\indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
- \indexml{Variable.import-thms}\verb|Variable.import_thms: bool -> thm list -> Proof.context ->|\isasep\isanewline%
+ \indexml{Variable.import\_thms}\verb|Variable.import_thms: bool -> thm list -> Proof.context ->|\isasep\isanewline%
\verb| ((ctyp list * cterm list) * thm list) * Proof.context| \\
\indexml{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
\end{mldecls}
@@ -235,9 +235,9 @@
\begin{mldecls}
\indexmltype{Assumption.export}\verb|type Assumption.export| \\
\indexml{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\
- \indexml{Assumption.add-assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline%
+ \indexml{Assumption.add\_assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline%
\verb| cterm list -> Proof.context -> thm list * Proof.context| \\
- \indexml{Assumption.add-assumes}\verb|Assumption.add_assumes: |\isasep\isanewline%
+ \indexml{Assumption.add\_assumes}\verb|Assumption.add_assumes: |\isasep\isanewline%
\verb| cterm list -> Proof.context -> thm list * Proof.context| \\
\indexml{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\
\end{mldecls}
@@ -333,7 +333,7 @@
\begin{mldecls}
\indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
- \indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
+ \indexml{Goal.prove\_multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
\end{mldecls}
\begin{mldecls}