doc-src/IsarImplementation/Thy/logic.thy
changeset 21324 a5089fc012b5
parent 20929 cd2a6d00ec47
child 21827 0b1d07f79c1e
     1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Mon Nov 13 15:42:58 2006 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Mon Nov 13 15:42:59 2006 +0100
     1.3 @@ -328,7 +328,7 @@
     1.4    @{index_ML betapply: "term * term -> term"} \\
     1.5    @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\
     1.6    @{index_ML Sign.add_abbrevs: "string * bool ->
     1.7 -  ((string * mixfix) * term) list -> theory -> theory"} \\
     1.8 +  ((string * mixfix) * term) list -> theory -> (term * term) list * theory"} \\
     1.9    @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
    1.10    @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
    1.11    \end{mldecls}