[isabelle-dev] New proof method "rewrite"

[Lars Noschinski]

On 18.03.2015 15:16, Lars Noschinski wrote:
> 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).
I've used it now a bit to add annotations in program verification and
(contrary to my former intuition) found the order of the patterns to be
the wrong way around.

If someone has used the rewrite method and has some opinions on that, I
would be glad to hear these.

  -- Lars