--- a/src/Pure/conv.ML Wed Mar 04 10:43:39 2009 +0100
+++ b/src/Pure/conv.ML Wed Mar 04 10:45:52 2009 +0100
@@ -7,12 +7,17 @@
infix 1 then_conv;
infix 0 else_conv;
+signature BASIC_CONV =
+sig
+ val then_conv: conv * conv -> conv
+ val else_conv: conv * conv -> conv
+end;
+
signature CONV =
sig
+ include BASIC_CONV
val no_conv: conv
val all_conv: conv
- val then_conv: conv * conv -> conv
- val else_conv: conv * conv -> conv
val first_conv: conv list -> conv
val every_conv: conv list -> conv
val try_conv: conv -> conv
@@ -171,3 +176,6 @@
| NONE => raise THM ("gconv_rule", i, [th]));
end;
+
+structure BasicConv: BASIC_CONV = Conv;
+open BasicConv;