Conditional Simplification

The article provides a collection of experimental general-purpose proof methods for the object logic Isabelle/HOL of the formal proof assistant Isabelle. The methods in the collection offer functionality that is similar to certain aspects of the functionality provided by the standard proof methods of Isabelle that combine classical reasoning and rewriting, such as the method auto, but use a different approach for rewriting. More specifically, these methods allow for the side conditions of the rewrite rules to be solved via intro-resolution.