doc-src/IsarImplementation/Thy/logic.thy
changeset 21827 0b1d07f79c1e
parent 21324 a5089fc012b5
child 22322 b9924abb8c66
     1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Wed Dec 13 15:47:37 2006 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Wed Dec 13 16:26:45 2006 +0100
     1.3 @@ -327,8 +327,7 @@
     1.4    @{index_ML lambda: "term -> term -> term"} \\
     1.5    @{index_ML betapply: "term * term -> term"} \\
     1.6    @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\
     1.7 -  @{index_ML Sign.add_abbrevs: "string * bool ->
     1.8 -  ((string * mixfix) * term) list -> theory -> (term * term) list * theory"} \\
     1.9 +  @{index_ML Sign.add_abbrev: "string -> bstring * term -> theory -> (term * term) * theory"} \\
    1.10    @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
    1.11    @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
    1.12    \end{mldecls}
    1.13 @@ -376,9 +375,8 @@
    1.14    \item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a
    1.15    new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
    1.16  
    1.17 -  \item @{ML Sign.add_abbrevs}~@{text "print_mode [((c, t), mx), \<dots>]"}
    1.18 -  declares a new term abbreviation @{text "c \<equiv> t"} with optional
    1.19 -  mixfix syntax.
    1.20 +  \item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"}
    1.21 +  introduces a new term abbreviation @{text "c \<equiv> t"}.
    1.22  
    1.23    \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
    1.24    Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}