replaced Sign.add_consts_i by Sign.declare_const;
authorwenzelm
Thu Oct 11 16:38:42 2007 +0200 (2007-10-11)
changeset 24972acafb18a47dc
parent 24971 4d006b03aa4a
child 24973 dc67846b00c0
replaced Sign.add_consts_i by Sign.declare_const;
doc-src/IsarImplementation/Thy/document/logic.tex
doc-src/IsarImplementation/Thy/logic.thy
     1.1 --- a/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Oct 11 16:05:56 2007 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Oct 11 16:38:42 2007 +0200
     1.3 @@ -328,8 +328,10 @@
     1.4    \indexml{fastype-of}\verb|fastype_of: term -> typ| \\
     1.5    \indexml{lambda}\verb|lambda: term -> term -> term| \\
     1.6    \indexml{betapply}\verb|betapply: term * term -> term| \\
     1.7 -  \indexml{Sign.add-consts-i}\verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory| \\
     1.8 -  \indexml{Sign.add-abbrev}\verb|Sign.add_abbrev: string -> Markup.property list -> bstring * term -> theory -> (term * term) * theory| \\
     1.9 +  \indexml{Sign.declare-const}\verb|Sign.declare_const: Markup.property list -> bstring * typ * mixfix ->|\isasep\isanewline%
    1.10 +\verb|  theory -> term * theory| \\
    1.11 +  \indexml{Sign.add-abbrev}\verb|Sign.add_abbrev: string -> Markup.property list -> bstring * term ->|\isasep\isanewline%
    1.12 +\verb|  theory -> (term * term) * theory| \\
    1.13    \indexml{Sign.const-typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
    1.14    \indexml{Sign.const-instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
    1.15    \end{mldecls}
    1.16 @@ -366,8 +368,9 @@
    1.17    \item \verb|betapply|~\isa{{\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}} produces an application \isa{t\ u}, with topmost \isa{{\isasymbeta}}-conversion if \isa{t} is an
    1.18    abstraction.
    1.19  
    1.20 -  \item \verb|Sign.add_consts_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares a
    1.21 -  new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix syntax.
    1.22 +  \item \verb|Sign.declare_const|~\isa{properties\ {\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharcomma}\ mx{\isacharparenright}}
    1.23 +  declares a new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix
    1.24 +  syntax.
    1.25  
    1.26    \item \verb|Sign.add_abbrev|~\isa{print{\isacharunderscore}mode\ properties\ {\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}}
    1.27    introduces a new term abbreviation \isa{c\ {\isasymequiv}\ t}.
     2.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Oct 11 16:05:56 2007 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Oct 11 16:38:42 2007 +0200
     2.3 @@ -326,8 +326,10 @@
     2.4    @{index_ML fastype_of: "term -> typ"} \\
     2.5    @{index_ML lambda: "term -> term -> term"} \\
     2.6    @{index_ML betapply: "term * term -> term"} \\
     2.7 -  @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\
     2.8 -  @{index_ML Sign.add_abbrev: "string -> Markup.property list -> bstring * term -> theory -> (term * term) * theory"} \\
     2.9 +  @{index_ML Sign.declare_const: "Markup.property list -> bstring * typ * mixfix ->
    2.10 +  theory -> term * theory"} \\
    2.11 +  @{index_ML Sign.add_abbrev: "string -> Markup.property list -> bstring * term ->
    2.12 +  theory -> (term * term) * theory"} \\
    2.13    @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
    2.14    @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
    2.15    \end{mldecls}
    2.16 @@ -372,8 +374,9 @@
    2.17    "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
    2.18    abstraction.
    2.19  
    2.20 -  \item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a
    2.21 -  new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
    2.22 +  \item @{ML Sign.declare_const}~@{text "properties (c, \<sigma>, mx)"}
    2.23 +  declares a new constant @{text "c :: \<sigma>"} with optional mixfix
    2.24 +  syntax.
    2.25  
    2.26    \item @{ML Sign.add_abbrev}~@{text "print_mode properties (c, t)"}
    2.27    introduces a new term abbreviation @{text "c \<equiv> t"}.