Dear All,
I am looking at higher-order rewriting. The cleanest way to implement it will
involve adding an extra parameter to the functions prim_rewrite_conv,
prim_rewrite_rule and prim_rewrite_tac (which I suspect aren't very widely
used). The parameter value will be optional and supplying Nil will give the
same behaviour as currently. If anybody has code that would be badly affected
by this, please let me know.
Regards,
Rob.
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
