src/Pure/conv.ML
changeset 30136 6a874aedb964
parent 29606 fedb8be05f24
child 32843 c8f5a7c8353f
     1.1 --- a/src/Pure/conv.ML	Thu Feb 26 17:42:43 2009 +0100
     1.2 +++ b/src/Pure/conv.ML	Thu Feb 26 18:00:08 2009 +0100
     1.3 @@ -7,12 +7,17 @@
     1.4  infix 1 then_conv;
     1.5  infix 0 else_conv;
     1.6  
     1.7 +signature BASIC_CONV =
     1.8 +sig
     1.9 +  val then_conv: conv * conv -> conv
    1.10 +  val else_conv: conv * conv -> conv
    1.11 +end;
    1.12 +
    1.13  signature CONV =
    1.14  sig
    1.15 +  include BASIC_CONV
    1.16    val no_conv: conv
    1.17    val all_conv: conv
    1.18 -  val then_conv: conv * conv -> conv
    1.19 -  val else_conv: conv * conv -> conv
    1.20    val first_conv: conv list -> conv
    1.21    val every_conv: conv list -> conv
    1.22    val try_conv: conv -> conv
    1.23 @@ -171,3 +176,6 @@
    1.24    | NONE => raise THM ("gconv_rule", i, [th]));
    1.25  
    1.26  end;
    1.27 +
    1.28 +structure BasicConv: BASIC_CONV = Conv;
    1.29 +open BasicConv;