doc-src/IsarImplementation/Thy/logic.thy
changeset 24972 acafb18a47dc
parent 24828 137c242e7277
child 26872 336dfd860744
--- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Oct 11 16:05:56 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Oct 11 16:38:42 2007 +0200
@@ -326,8 +326,10 @@
   @{index_ML fastype_of: "term -> typ"} \\
   @{index_ML lambda: "term -> term -> term"} \\
   @{index_ML betapply: "term * term -> term"} \\
-  @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\
-  @{index_ML Sign.add_abbrev: "string -> Markup.property list -> bstring * term -> theory -> (term * term) * theory"} \\
+  @{index_ML Sign.declare_const: "Markup.property list -> bstring * typ * mixfix ->
+  theory -> term * theory"} \\
+  @{index_ML Sign.add_abbrev: "string -> Markup.property list -> bstring * term ->
+  theory -> (term * term) * theory"} \\
   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
   \end{mldecls}
@@ -372,8 +374,9 @@
   "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
   abstraction.
 
-  \item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a
-  new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
+  \item @{ML Sign.declare_const}~@{text "properties (c, \<sigma>, mx)"}
+  declares a new constant @{text "c :: \<sigma>"} with optional mixfix
+  syntax.
 
   \item @{ML Sign.add_abbrev}~@{text "print_mode properties (c, t)"}
   introduces a new term abbreviation @{text "c \<equiv> t"}.