doc-src/IsarImplementation/Thy/Logic.thy

   @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
   @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
   @{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}
 
   \item @{ML_type ctyp} and @{ML_type cterm} represent certified types