Implementing in Isabelle: adding structure at the metalevel
In TACAS, pages
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
Max-Planck-Inst., Saarbrucken, Germany.
Available as PostScript,
BRICS WWW home page