@Article{BasinMatthewsMetaInd,
author        = {David Basin and Sean Matthews},
title         = {Structuring Metatheory on Inductive Definitions},
journal       = {Information and Computation},
month      = {October/November},
year          = {2000},
Volume        = {162},
Number       = {1--2},
page = {80--95},
abstract      = {
We examine a problem for machine supported metatheory.  There are
statements true about a theory that are true of some (but only some)
extensions; however standard theory-structuring facilities do not
support selective inheritance.  We use the example of the deduction
theorem for modal logic and show how a statement about a theory can
explicitly formalize the closure conditions extensions should
satisfy for it to remain true.  We show how metatheories based on
inductive definitions allow theories and general metatheorems to be
organized hierarchically this way, and report on a case study using
the theory FS0.
}		  
}