320 \end{mldecls} |
320 \end{mldecls} |
321 \begin{mldecls} |
321 \begin{mldecls} |
322 @{index_ML fastype_of: "term -> typ"} \\ |
322 @{index_ML fastype_of: "term -> typ"} \\ |
323 @{index_ML lambda: "term -> term -> term"} \\ |
323 @{index_ML lambda: "term -> term -> term"} \\ |
324 @{index_ML betapply: "term * term -> term"} \\ |
324 @{index_ML betapply: "term * term -> term"} \\ |
325 @{index_ML Sign.declare_const: "Properties.T -> (binding * typ) * mixfix -> |
325 @{index_ML Sign.declare_const: "(binding * typ) * mixfix -> |
326 theory -> term * theory"} \\ |
326 theory -> term * theory"} \\ |
327 @{index_ML Sign.add_abbrev: "string -> Properties.T -> binding * term -> |
327 @{index_ML Sign.add_abbrev: "string -> binding * term -> |
328 theory -> (term * term) * theory"} \\ |
328 theory -> (term * term) * theory"} \\ |
329 @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\ |
329 @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\ |
330 @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\ |
330 @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\ |
331 \end{mldecls} |
331 \end{mldecls} |
332 |
332 |
368 |
368 |
369 \item @{ML betapply}~@{text "(t, u)"} produces an application @{text |
369 \item @{ML betapply}~@{text "(t, u)"} produces an application @{text |
370 "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an |
370 "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an |
371 abstraction. |
371 abstraction. |
372 |
372 |
373 \item @{ML Sign.declare_const}~@{text "properties ((c, \<sigma>), mx)"} |
373 \item @{ML Sign.declare_const}~@{text "((c, \<sigma>), mx)"} |
374 declares a new constant @{text "c :: \<sigma>"} with optional mixfix |
374 declares a new constant @{text "c :: \<sigma>"} with optional mixfix |
375 syntax. |
375 syntax. |
376 |
376 |
377 \item @{ML Sign.add_abbrev}~@{text "print_mode properties (c, t)"} |
377 \item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"} |
378 introduces a new term abbreviation @{text "c \<equiv> t"}. |
378 introduces a new term abbreviation @{text "c \<equiv> t"}. |
379 |
379 |
380 \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML |
380 \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML |
381 Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"} |
381 Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"} |
382 convert between two representations of polymorphic constants: full |
382 convert between two representations of polymorphic constants: full |