doc-src/IsarImplementation/Thy/logic.thy
changeset 21827 0b1d07f79c1e
parent 21324 a5089fc012b5
child 22322 b9924abb8c66
equal deleted inserted replaced
21826:b90d927e0a4b 21827:0b1d07f79c1e
   325   \begin{mldecls}
   325   \begin{mldecls}
   326   @{index_ML fastype_of: "term -> typ"} \\
   326   @{index_ML fastype_of: "term -> typ"} \\
   327   @{index_ML lambda: "term -> term -> term"} \\
   327   @{index_ML lambda: "term -> term -> term"} \\
   328   @{index_ML betapply: "term * term -> term"} \\
   328   @{index_ML betapply: "term * term -> term"} \\
   329   @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\
   329   @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\
   330   @{index_ML Sign.add_abbrevs: "string * bool ->
   330   @{index_ML Sign.add_abbrev: "string -> bstring * term -> theory -> (term * term) * theory"} \\
   331   ((string * mixfix) * term) list -> theory -> (term * term) list * theory"} \\
       
   332   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
   331   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
   333   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
   332   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
   334   \end{mldecls}
   333   \end{mldecls}
   335 
   334 
   336   \begin{description}
   335   \begin{description}
   374   abstraction.
   373   abstraction.
   375 
   374 
   376   \item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a
   375   \item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a
   377   new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
   376   new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
   378 
   377 
   379   \item @{ML Sign.add_abbrevs}~@{text "print_mode [((c, t), mx), \<dots>]"}
   378   \item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"}
   380   declares a new term abbreviation @{text "c \<equiv> t"} with optional
   379   introduces a new term abbreviation @{text "c \<equiv> t"}.
   381   mixfix syntax.
       
   382 
   380 
   383   \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
   381   \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
   384   Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}
   382   Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}
   385   convert between two representations of polymorphic constants: full
   383   convert between two representations of polymorphic constants: full
   386   type instance vs.\ compact type arguments form.
   384   type instance vs.\ compact type arguments form.