Implementation of a pattern-based substitution method for Isabelle.
See the PatSubstWalkthrough.thy file for examples of how to use the method.
This proof method has now been integrated into the main Isabelle distribution as ~~/src/HOL/Library/Rewrite and will be available with the 2015 release. This repository now only remains for historical reasons.