Email Gateway (Aug 18 2022 at 11:07): Email Gateway (Aug 18 2022 at 11:07):From: Clemens Ballarin <ballarin@in.tum.de>
A new locales tutorial (for Isabelle 2007) is now available:
Clemens Ballarin. Tutorial to Locales and Locale Interpretation.
Technical Report TUM-I0723, Technische Universität München, 2007.
http://www4.in.tum.de/~ballarin/publications/TUM-I0723.pdf
Abstract:
Locales are Isabelle's mechanism to deal with parametric
theories. We present typical examples of locale specifications,
along with interpretations between locales to change their
hierarchic dependencies and interpretations to reuse locales in
theory contexts and proofs.
This tutorial is intended for locale novices; familiarity with
Isabelle and Isar is presumed.
Cheers,
Clemens
Last updated: May 03 2024 at 08:18 UTC