Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use binding type;
authorwenzelm
Sun, 08 Mar 2009 00:41:52 +0100
changeset 30355 8066d80cd51e
parent 30354 0d037d7e2a75
child 30356 36d0e00af606
use binding type;
doc-src/IsarImplementation/Thy/Logic.thy file | annotate | diff | comparison | revisions
doc-src/IsarImplementation/Thy/document/Logic.tex file | annotate | diff | comparison | revisions 
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Sun Mar 08 00:16:34 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Sun Mar 08 00:41:52 2009 +0100
@@ -126,10 +126,10 @@
   \begin{mldecls}
   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
-  @{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\
+  @{index_ML Sign.add_types: "(binding * int * mixfix) list -> theory -> theory"} \\
   @{index_ML Sign.add_tyabbrs_i: "
-  (string * string list * typ * mixfix) list -> theory -> theory"} \\
-  @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
+  (binding * string list * typ * mixfix) list -> theory -> theory"} \\
+  @{index_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\
   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
   \end{mldecls}
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Sun Mar 08 00:16:34 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Sun Mar 08 00:41:52 2009 +0100
@@ -137,10 +137,10 @@
   \begin{mldecls}
   \indexdef{}{ML}{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
   \indexdef{}{ML}{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
-  \indexdef{}{ML}{Sign.add\_types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\
+  \indexdef{}{ML}{Sign.add\_types}\verb|Sign.add_types: (binding * int * mixfix) list -> theory -> theory| \\
   \indexdef{}{ML}{Sign.add\_tyabbrs\_i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline%
-\verb|  (string * string list * typ * mixfix) list -> theory -> theory| \\
-  \indexdef{}{ML}{Sign.primitive\_class}\verb|Sign.primitive_class: string * class list -> theory -> theory| \\
+\verb|  (binding * string list * typ * mixfix) list -> theory -> theory| \\
+  \indexdef{}{ML}{Sign.primitive\_class}\verb|Sign.primitive_class: binding * class list -> theory -> theory| \\
   \indexdef{}{ML}{Sign.primitive\_classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
   \indexdef{}{ML}{Sign.primitive\_arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
   \end{mldecls}
isabelle