--- a/src/Pure/conv.ML Thu May 31 18:16:59 2007 +0200
+++ b/src/Pure/conv.ML Thu May 31 18:31:36 2007 +0200
@@ -7,11 +7,10 @@
infix 1 then_conv;
infix 0 else_conv;
-infix aconvc;
+
signature CONV =
sig
type conv = cterm -> thm
- val aconvc : cterm * cterm -> bool
val no_conv: conv
val all_conv: conv
val then_conv: conv * conv -> conv
@@ -43,8 +42,6 @@
type conv = cterm -> thm;
-fun s aconvc t = term_of s aconv term_of t;
-
fun no_conv _ = raise CTERM ("no conversion", []);
val all_conv = Thm.reflexive;
@@ -106,6 +103,7 @@
fun binop_conv cv = combination_conv (arg_conv cv) cv;
+
(* logic *)
(*rewrite B in !!x1 ... xn. B*)
--- 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;