[isabelle-dev] New proof method "rewrite"
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 . 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).
More information about the isabelle-dev