equal
deleted
inserted
replaced
323 \end{mldecls} |
323 \end{mldecls} |
324 \begin{mldecls} |
324 \begin{mldecls} |
325 \indexdef{}{ML}{fastype\_of}\verb|fastype_of: term -> typ| \\ |
325 \indexdef{}{ML}{fastype\_of}\verb|fastype_of: term -> typ| \\ |
326 \indexdef{}{ML}{lambda}\verb|lambda: term -> term -> term| \\ |
326 \indexdef{}{ML}{lambda}\verb|lambda: term -> term -> term| \\ |
327 \indexdef{}{ML}{betapply}\verb|betapply: term * term -> term| \\ |
327 \indexdef{}{ML}{betapply}\verb|betapply: term * term -> term| \\ |
328 \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix ->|\isasep\isanewline% |
328 \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: (binding * typ) * mixfix ->|\isasep\isanewline% |
329 \verb| theory -> term * theory| \\ |
329 \verb| theory -> term * theory| \\ |
330 \indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> binding * term ->|\isasep\isanewline% |
330 \indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> binding * term ->|\isasep\isanewline% |
331 \verb| theory -> (term * term) * theory| \\ |
331 \verb| theory -> (term * term) * theory| \\ |
332 \indexdef{}{ML}{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\ |
332 \indexdef{}{ML}{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\ |
333 \indexdef{}{ML}{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\ |
333 \indexdef{}{ML}{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\ |
334 \end{mldecls} |
334 \end{mldecls} |
335 |
335 |
363 body \isa{b} are replaced by bound variables. |
363 body \isa{b} are replaced by bound variables. |
364 |
364 |
365 \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 |
365 \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 |
366 abstraction. |
366 abstraction. |
367 |
367 |
368 \item \verb|Sign.declare_const|~\isa{properties\ {\isacharparenleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharparenright}{\isacharcomma}\ mx{\isacharparenright}} |
368 \item \verb|Sign.declare_const|~\isa{{\isacharparenleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharparenright}{\isacharcomma}\ mx{\isacharparenright}} |
369 declares a new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix |
369 declares a new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix |
370 syntax. |
370 syntax. |
371 |
371 |
372 \item \verb|Sign.add_abbrev|~\isa{print{\isacharunderscore}mode\ properties\ {\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}} |
372 \item \verb|Sign.add_abbrev|~\isa{print{\isacharunderscore}mode\ {\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. |