[isabelle-dev] New proof method "rewrite"

Lars Noschinski noschinl at in.tum.de
Wed Mar 18 15:16:56 CET 2015


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/

More information about the isabelle-dev mailing list