src/Pure/more_thm.ML

     ID:         $Id$
     Author:     Makarius
 
 Further operations on type ctyp/cterm/thm, outside the inference kernel.
 *)
+
+infix aconvc;
 
 signature THM =
 sig
   include THM
   val mk_binop: cterm -> cterm -> cterm -> cterm

   val dest_equals_lhs: cterm -> cterm
   val dest_equals_rhs: cterm -> cterm
   val lhs_of: thm -> cterm
   val rhs_of: thm -> cterm
   val thm_ord: thm * thm -> order
+  val aconvc : cterm * cterm -> bool
   val eq_thm: thm * thm -> bool
   val eq_thms: thm list * thm list -> bool
   val eq_thm_thy: thm * thm -> bool
   val eq_thm_prop: thm * thm -> bool
   val equiv_thm: thm * thm -> bool

     | ord => ord)
   end;
 
 
 (* equality *)
+
+val op aconvc = op aconv o pairself Thm.term_of;
 
 fun eq_thm ths =
   Context.joinable (pairself Thm.theory_of_thm ths) andalso
   thm_ord ths = EQUAL;