related.tex

NOTE: Matt has expanded the first paragraph of the introduction to
mention some related work, and suggests that we not have a related
work section.  The wording in the intro now makes it clear (hopefully)
that this paper is about an extension, so presumably related work
would be found in preceding papers.

{\it \color{red} MATT will write this (but will welcome any ideas from
  Sol):

\begin{enumerate}

\item Boyer-Moore paper~\cite{meta}
\item ACL2 paper on meta~\cite{meta-05}
\item Milawa?~\cite{davis09}

\end{enumerate}

Probably we should give a nod to other ITP systems that do meta, but
I'm not sure and I don't know what they are.  Maybe I'll look in
\cite{meta-05}.  I thought of pointing to Harrison's book, but the
table of contents at http://www.gbv.de/dms/ilmenau/toc/585835187.PDF
seem not to have anything about meta.

% @book{Harrison:2009:HPL:1540610,
%  author = {Harrison, John},
%  title = {Handbook of Practical Logic and Automated Reasoning},
%  year = {2009},
%  isbn = {0521899575, 9780521899574},
%  edition = {1st},
%  publisher = {Cambridge University Press},
%  address = {New York, NY, USA},
% }

}