--- a/src/Pure/more_thm.ML Thu May 31 18:16:59 2007 +0200
+++ b/src/Pure/more_thm.ML Thu May 31 18:31:36 2007 +0200
@@ -5,6 +5,8 @@
Further operations on type ctyp/cterm/thm, outside the inference kernel.
*)
+infix aconvc;
+
signature THM =
sig
include THM
@@ -17,6 +19,7 @@
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
@@ -99,6 +102,8 @@
(* 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;