Interactive theorem proving with schematic theory specific rules

This work presents a framework to make interactive proving over abstract data types (first order logic plus induction) more comfortable. A language of schematic rules is introduced, yielding the ability to write, to use, and even to verify these rules for any abstract data type and its theory. The language allows to express the functionality of a rule easily and clearly. Nearly all potential rule applications are coupled with the occurrence of certain terms or formulas. One can prove with these rules simply by mouse clicks onto these terms and formulas. The rule language is expressive enough to describe even complex induction rules. Nevertheless, the correctness of a rule can be verified within the same theory without use of explicit higher order logic or of a translation to some kind of meta level. So, in each state of a proof, new rules can be introduced, whenever required, and proven.