[isabelle-dev] New proof method "rewrite"

[Lars Noschinski]

Hi,

commit 4ed50ebf5d36 adds a new proof method "rewrite". This is the
pattern-based replacement for subst Christoph Traut and I presented at
the last Isabelle Workshop [1]. For now, it lifes in
~~/src/HOL/Library/Rewrite and is still missing a proper documentation
(but there are examples in ~~/src/HOL/ex/Rewrite_Examples).

The plan is to eventually move it into the main HOL image (although
technically it should work with any logic with a simplifier setup).


[1] https://www21.in.tum.de/~noschinl/Pattern-2014/