src/Pure/conv.ML
changeset 23169 37091da05d8e
parent 23034 b3a6815754d6
child 23411 c524900454f3
     1.1 --- a/src/Pure/conv.ML	Thu May 31 18:16:59 2007 +0200
     1.2 +++ b/src/Pure/conv.ML	Thu May 31 18:31:36 2007 +0200
     1.3 @@ -7,11 +7,10 @@
     1.4  
     1.5  infix 1 then_conv;
     1.6  infix 0 else_conv;
     1.7 -infix aconvc;
     1.8 +
     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 @@ -43,8 +42,6 @@
    1.17  
    1.18  type conv = cterm -> thm;
    1.19  
    1.20 -fun s aconvc t = term_of s aconv term_of t;
    1.21 -
    1.22  fun no_conv _ = raise CTERM ("no conversion", []);
    1.23  val all_conv = Thm.reflexive;
    1.24  
    1.25 @@ -106,6 +103,7 @@
    1.26  
    1.27  fun binop_conv cv = combination_conv (arg_conv cv) cv;
    1.28  
    1.29 +
    1.30  (* logic *)
    1.31  
    1.32  (*rewrite B in !!x1 ... xn. B*)