# HG changeset patch
# User chaieb
# Date 1179591585 -7200
# Node ID b3a6815754d6fd8b7a9f7d299e8df4cebb93d7c2
# Parent  a7e23f993c5e00ae0fb14ced4b3d73abc2dad8b0
added binop_conv, aconvc

diff -r a7e23f993c5e -r b3a6815754d6 src/Pure/conv.ML
--- a/src/Pure/conv.ML	Sat May 19 18:19:06 2007 +0200
+++ b/src/Pure/conv.ML	Sat May 19 18:19:45 2007 +0200
@@ -7,10 +7,11 @@
 
 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
@@ -27,6 +28,7 @@
   val fun_conv: conv -> conv
   val arg1_conv: conv -> conv
   val fun2_conv: conv -> conv
+  val binop_conv: conv -> conv
   val forall_conv: int -> conv -> conv
   val concl_conv: int -> conv -> conv
   val prems_conv: int -> (int -> conv) -> conv
@@ -41,6 +43,8 @@
 
 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;
 
@@ -100,6 +104,7 @@
 val arg1_conv = fun_conv o arg_conv;
 val fun2_conv = fun_conv o fun_conv;
 
+fun binop_conv cv = combination_conv (arg_conv cv) cv;
 
 (* logic *)