Re: [isabelle] Isabelle2015-RC1: Rule instantiation in Eisbach



On Thu, 23 Apr 2015, Daniel Matichuk wrote:

There is some argument for extending the match pattern language to support more precise term deconstruction, but I'm waiting to see more use cases before adding more complexity.

It would be interesting to explore the question if/how the new "rewrite" method facilities could be re-used here.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.