@article{Basin&Matthews96,
AUTHOR        = {David Basin and Sean Matthews},
title = "Adding Metatheoretic Facilities to First-order Theories",
journal = "Journal of Logic and Computation",
volume = 6,
number = 6,
year = "1996",
pages = "835--849",
Abstract = {
Generic proof systems like Isabelle provide some limited but useful
metatheoretic facilities for declared logics; in particular, users
can prove simple derived rules and also `solve' formulae that contain
metavariables --- a technique useful for, e.g., program synthesis.  
We show how an arbitrary first order theory can be
conservatively extended to provide similar facilities, without a
supporting metatheory, and examine what the limitations of this
approach are. },
}