equal
deleted
inserted
replaced
327 \begin{mldecls} |
327 \begin{mldecls} |
328 \indexml{fastype-of}\verb|fastype_of: term -> typ| \\ |
328 \indexml{fastype-of}\verb|fastype_of: term -> typ| \\ |
329 \indexml{lambda}\verb|lambda: term -> term -> term| \\ |
329 \indexml{lambda}\verb|lambda: term -> term -> term| \\ |
330 \indexml{betapply}\verb|betapply: term * term -> term| \\ |
330 \indexml{betapply}\verb|betapply: term * term -> term| \\ |
331 \indexml{Sign.add-consts-i}\verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory| \\ |
331 \indexml{Sign.add-consts-i}\verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory| \\ |
332 \indexml{Sign.add-abbrev}\verb|Sign.add_abbrev: string -> bstring * term -> theory -> (term * term) * theory| \\ |
332 \indexml{Sign.add-abbrev}\verb|Sign.add_abbrev: string -> Markup.property list -> bstring * term -> theory -> (term * term) * theory| \\ |
333 \indexml{Sign.const-typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\ |
333 \indexml{Sign.const-typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\ |
334 \indexml{Sign.const-instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\ |
334 \indexml{Sign.const-instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\ |
335 \end{mldecls} |
335 \end{mldecls} |
336 |
336 |
337 \begin{description} |
337 \begin{description} |
367 abstraction. |
367 abstraction. |
368 |
368 |
369 \item \verb|Sign.add_consts_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares a |
369 \item \verb|Sign.add_consts_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares a |
370 new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix syntax. |
370 new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix syntax. |
371 |
371 |
372 \item \verb|Sign.add_abbrev|~\isa{print{\isacharunderscore}mode\ {\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}} |
372 \item \verb|Sign.add_abbrev|~\isa{print{\isacharunderscore}mode\ properties\ {\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}} |
373 introduces a new term abbreviation \isa{c\ {\isasymequiv}\ t}. |
373 introduces a new term abbreviation \isa{c\ {\isasymequiv}\ t}. |
374 |
374 |
375 \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}} |
375 \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}} |
376 convert between two representations of polymorphic constants: full |
376 convert between two representations of polymorphic constants: full |
377 type instance vs.\ compact type arguments form. |
377 type instance vs.\ compact type arguments form. |