--- a/doc-src/IsarImplementation/Thy/document/logic.tex Wed Dec 13 15:47:37 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex Wed Dec 13 16:26:45 2006 +0100
@@ -329,8 +329,7 @@
\indexml{lambda}\verb|lambda: term -> term -> term| \\
\indexml{betapply}\verb|betapply: term * term -> term| \\
\indexml{Sign.add-consts-i}\verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory| \\
- \indexml{Sign.add-abbrevs}\verb|Sign.add_abbrevs: string * bool ->|\isasep\isanewline%
-\verb| ((string * mixfix) * term) list -> theory -> (term * term) list * theory| \\
+ \indexml{Sign.add-abbrev}\verb|Sign.add_abbrev: string -> bstring * term -> theory -> (term * term) * theory| \\
\indexml{Sign.const-typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
\indexml{Sign.const-instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
\end{mldecls}
@@ -370,9 +369,8 @@
\item \verb|Sign.add_consts_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares a
new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix syntax.
- \item \verb|Sign.add_abbrevs|~\isa{print{\isacharunderscore}mode\ {\isacharbrackleft}{\isacharparenleft}{\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}}
- declares a new term abbreviation \isa{c\ {\isasymequiv}\ t} with optional
- mixfix syntax.
+ \item \verb|Sign.add_abbrev|~\isa{print{\isacharunderscore}mode\ {\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}}
+ introduces a new term abbreviation \isa{c\ {\isasymequiv}\ t}.
\item \verb|Sign.const_typargs|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} and \verb|Sign.const_instance|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharbrackright}{\isacharparenright}}
convert between two representations of polymorphic constants: full