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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to