--- a/doc-src/IsarImplementation/Thy/Logic.thy Fri Oct 01 17:23:26 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Thu Oct 07 12:39:01 2010 +0100
@@ -552,12 +552,14 @@
@{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
@{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
@{index_ML Thm.add_axiom: "binding * term -> theory -> (string * thm) * theory"} \\
- @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory
- -> (string * ('a -> thm)) * theory"} \\
- @{index_ML Thm.add_def: "bool -> bool -> binding * term -> theory -> (string * thm) * theory"} \\
+ @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->
+ (string * ('a -> thm)) * theory"} \\
+ @{index_ML Thm.add_def: "bool -> bool -> binding * term -> theory ->
+ (string * thm) * theory"} \\
\end{mldecls}
\begin{mldecls}
- @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
+ @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list ->
+ theory -> theory"} \\
\end{mldecls}
\begin{description}