--- 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*)