added binop_conv, aconvc
authorchaieb
Sat May 19 18:19:45 2007 +0200 (2007-05-19)
changeset 23034b3a6815754d6
parent 23033 a7e23f993c5e
child 23035 643859163183
added binop_conv, aconvc
src/Pure/conv.ML
     1.1 --- a/src/Pure/conv.ML	Sat May 19 18:19:06 2007 +0200
     1.2 +++ b/src/Pure/conv.ML	Sat May 19 18:19:45 2007 +0200
     1.3 @@ -7,10 +7,11 @@
     1.4  
     1.5  infix 1 then_conv;
     1.6  infix 0 else_conv;
     1.7 -
     1.8 +infix aconvc;
     1.9  signature CONV =
    1.10  sig
    1.11    type conv = cterm -> thm
    1.12 +  val aconvc : cterm * cterm -> bool
    1.13    val no_conv: conv
    1.14    val all_conv: conv
    1.15    val then_conv: conv * conv -> conv
    1.16 @@ -27,6 +28,7 @@
    1.17    val fun_conv: conv -> conv
    1.18    val arg1_conv: conv -> conv
    1.19    val fun2_conv: conv -> conv
    1.20 +  val binop_conv: conv -> conv
    1.21    val forall_conv: int -> conv -> conv
    1.22    val concl_conv: int -> conv -> conv
    1.23    val prems_conv: int -> (int -> conv) -> conv
    1.24 @@ -41,6 +43,8 @@
    1.25  
    1.26  type conv = cterm -> thm;
    1.27  
    1.28 +fun s aconvc t = term_of s aconv term_of t;
    1.29 +
    1.30  fun no_conv _ = raise CTERM ("no conversion", []);
    1.31  val all_conv = Thm.reflexive;
    1.32  
    1.33 @@ -100,6 +104,7 @@
    1.34  val arg1_conv = fun_conv o arg_conv;
    1.35  val fun2_conv = fun_conv o fun_conv;
    1.36  
    1.37 +fun binop_conv cv = combination_conv (arg_conv cv) cv;
    1.38  
    1.39  (* logic *)
    1.40