src/Pure/more_thm.ML
changeset 24948 c12c16a680a0
parent 24775 4f86d3384111
child 24980 16a74cfca971
equal deleted inserted replaced
24947:b7e990e1706a 24948:c12c16a680a0
     8 infix aconvc;
     8 infix aconvc;
     9 
     9 
    10 signature THM =
    10 signature THM =
    11 sig
    11 sig
    12   include THM
    12   include THM
    13   val aconvc : cterm * cterm -> bool
    13   val aconvc: cterm * cterm -> bool
    14   val add_cterm_frees: cterm -> cterm list -> cterm list
    14   val add_cterm_frees: cterm -> cterm list -> cterm list
    15   val mk_binop: cterm -> cterm -> cterm -> cterm
    15   val mk_binop: cterm -> cterm -> cterm -> cterm
    16   val dest_binop: cterm -> cterm * cterm
    16   val dest_binop: cterm -> cterm * cterm
    17   val dest_implies: cterm -> cterm * cterm
    17   val dest_implies: cterm -> cterm * cterm
    18   val dest_equals: cterm -> cterm * cterm
    18   val dest_equals: cterm -> cterm * cterm