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.