Implementing in Isabelle: adding structure at the metalevel

Seán Matthews

In TACAS, pages 146--158


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, DVI.

[BRICS symbol] BRICS WWW home page