doc-src/IsarImplementation/Thy/prelim.thy
changeset 20547 796ae7fa1049
parent 20530 448594cbd82b
child 21852 7f2853bd54bf
--- a/doc-src/IsarImplementation/Thy/prelim.thy	Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/prelim.thy	Fri Sep 15 22:56:08 2006 +0200
@@ -152,7 +152,9 @@
   @{index_ML Theory.subthy: "theory * theory -> bool"} \\
   @{index_ML Theory.merge: "theory * theory -> theory"} \\
   @{index_ML Theory.checkpoint: "theory -> theory"} \\
-  @{index_ML Theory.copy: "theory -> theory"} \\[1ex]
+  @{index_ML Theory.copy: "theory -> theory"} \\
+  \end{mldecls}
+  \begin{mldecls}
   @{index_ML_type theory_ref} \\
   @{index_ML Theory.self_ref: "theory -> theory_ref"} \\
   @{index_ML Theory.deref: "theory_ref -> theory"} \\
@@ -480,7 +482,9 @@
   @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
   @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
   @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
-  @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\[1ex]
+  @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
+  \end{mldecls}
+  \begin{mldecls}
   @{index_ML_type "Symbol.sym"} \\
   @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
   \end{mldecls}
@@ -552,7 +556,9 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML Name.internal: "string -> string"} \\
-  @{index_ML Name.skolem: "string -> string"} \\[1ex]
+  @{index_ML Name.skolem: "string -> string"} \\
+  \end{mldecls}
+  \begin{mldecls}
   @{index_ML_type Name.context} \\
   @{index_ML Name.context: Name.context} \\
   @{index_ML Name.declare: "string -> Name.context -> Name.context"} \\
@@ -697,11 +703,15 @@
   @{index_ML NameSpace.qualifier: "string -> string"} \\
   @{index_ML NameSpace.append: "string -> string -> string"} \\
   @{index_ML NameSpace.pack: "string list -> string"} \\
-  @{index_ML NameSpace.unpack: "string -> string list"} \\[1ex]
+  @{index_ML NameSpace.unpack: "string -> string list"} \\
+  \end{mldecls}
+  \begin{mldecls}
   @{index_ML_type NameSpace.naming} \\
   @{index_ML NameSpace.default_naming: NameSpace.naming} \\
   @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
-  @{index_ML NameSpace.full: "NameSpace.naming -> string -> string"} \\[1ex]
+  @{index_ML NameSpace.full: "NameSpace.naming -> string -> string"} \\
+  \end{mldecls}
+  \begin{mldecls}
   @{index_ML_type NameSpace.T} \\
   @{index_ML NameSpace.empty: NameSpace.T} \\
   @{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\