Implementing in Isabelle: adding structure at the metalevel
Seán Matthews
In TACAS, pages
146--158
Abstract:
We show how a generic theorem prover like Isabelle can be used
to provide structuring facilties to a theory that lacks them, without our
having to modify the theory itself in any way
Comments
Max-Planck-Inst., Saarbrucken, Germany.
Available as PostScript,
DVI.
![[BRICS symbol]](http://www.brics.aau.dk/BRICS/GIF/BRICS/msymbol8mm.GIF)
BRICS WWW home page