Re: [isabelle] antiquotations
On Mon, 11 Feb 2008, Jeremy Dawson wrote:
> Finally, is all this stuff documented anywhere?
Here are some references that might help:
* Makarius Wenzel and Burkhart Wolff. Building Formal Method Tools in the
Isabelle/Isar Framework. In Theorem Proving in Higher Order Logics,
* Makarius Wenzel and Amine Chaieb. SML with antiquotations embedded into
Isabelle/Isar. In J. Carette and F. Wiedijk, editors. Programming
Languages for Mechanized Mathematics Workshop (CALCULEMUS 2007).
* Amine Chaieb and Makarius Wenzel. Context aware Calculation and
Deduction --- Ring Equalities via Gröbner Bases in Isabelle. In M.
Kauers, M. Kerber, R. Miner, and W. Windsteiger, editors. Towards
Mechanized Mathematical Assistants (CALCULEMUS 2007 and MKM 2007).
* Makarius Wenzel. The Isabelle/Isar Implementation Manual. Distributed
with Isabelle2007 (incomplete).
These things did not appear overnight out of the blue, but emerged from
principles that have been present in Isabelle for many years already.
The following talk provides an overview of the general state of affairs of
integrating everything into some kind of ``logical operating system'':
* Makarius Wenzel.
Aspects of locality in Isabelle --- local proofs, local theories, and
When using the system you do not have to understand all the details, but
merely sit back comfortably and let the framework do most of the job.
Complications mostly arise from trying to challange things by interfering
with the low-level implementation layer.
This archive was generated by a fusion of
Pipermail (Mailman edition) and