src/Pure/thm.ML
changeset 10767 8fa4aafa7314
parent 10486 7b07dd104a1a
child 11518 5f2616a1c10a
equal deleted inserted replaced
10766:ace2ba2d4fd1 10767:8fa4aafa7314
    25   val term_of           : cterm -> term
    25   val term_of           : cterm -> term
    26   val cterm_of          : Sign.sg -> term -> cterm
    26   val cterm_of          : Sign.sg -> term -> cterm
    27   val ctyp_of_term      : cterm -> ctyp
    27   val ctyp_of_term      : cterm -> ctyp
    28   val read_cterm        : Sign.sg -> string * typ -> cterm
    28   val read_cterm        : Sign.sg -> string * typ -> cterm
    29   val cterm_fun         : (term -> term) -> (cterm -> cterm)
    29   val cterm_fun         : (term -> term) -> (cterm -> cterm)
    30   val dest_comb         : cterm -> cterm * cterm
       
    31   val dest_abs          : string option -> cterm -> cterm * cterm
       
    32   val adjust_maxidx     : cterm -> cterm
    30   val adjust_maxidx     : cterm -> cterm
    33   val capply            : cterm -> cterm -> cterm
       
    34   val cabs              : cterm -> cterm -> cterm
       
    35   val read_def_cterm    :
    31   val read_def_cterm    :
    36     Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    32     Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    37     string list -> bool -> string * typ -> cterm * (indexname * typ) list
    33     string list -> bool -> string * typ -> cterm * (indexname * typ) list
    38   val read_def_cterms   :
    34   val read_def_cterms   :
    39     Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    35     Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
   151 end;
   147 end;
   152 
   148 
   153 signature THM =
   149 signature THM =
   154 sig
   150 sig
   155   include BASIC_THM
   151   include BASIC_THM
       
   152   val dest_comb         : cterm -> cterm * cterm
       
   153   val dest_abs          : string option -> cterm -> cterm * cterm
       
   154   val capply            : cterm -> cterm -> cterm
       
   155   val cabs              : cterm -> cterm -> cterm
   156   val major_prem_of	: thm -> term
   156   val major_prem_of	: thm -> term
   157   val no_prems		: thm -> bool
   157   val no_prems		: thm -> bool
   158   val no_attributes	: 'a -> 'a * 'b attribute list
   158   val no_attributes	: 'a -> 'a * 'b attribute list
   159   val apply_attributes	: ('a * thm) * 'a attribute list -> ('a * thm)
   159   val apply_attributes	: ('a * thm) * 'a attribute list -> ('a * thm)
   160   val applys_attributes	: ('a * thm list) * 'a attribute list -> ('a * thm list)
   160   val applys_attributes	: ('a * thm list) * 'a attribute list -> ('a * thm list)