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/ _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
