Email Gateway (Oct 29 2020 at 13:49): Email Gateway (Oct 29 2020 at 13:49):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Self-contained library theory "Word" taken over from former session
"HOL-Word".
Former session "HOL-Word": Misc ancient material has been factored out
into separate theories and moved to session Word_Lib in the AFP. See
theory "Guide" there for further information. INCOMPATIBILITY.
This refers to Isabelle/c7038c397ae3 and AFP/1d9680ca2b5.
I finally decided to take this step already before the next release
since the division between HOL-Word and Word_Lib is historical and
artificial and prevents organisation of the existing material.
Currently I plan some more streamlining, particularly more telling
theory names, which will be reflected in Guide.thy accordingly.
With Isabelle2021 planned for February 2021, there is still some time
for early adopters to have a look at the current matter of affairs.
Cheers,
Florian
signature.asc
Email Gateway (Jun 16 2021 at 11:17):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
"global_interpretation" is applicable in instantiation and overloading
targets and in any nested target built on top of a target supporting
"global_interpretation".
Using "global_interpretation" in instantiation targets provides a direct
way to transfer logical relations in the module system to type class
instances and can emulate the concept of default type class instances
from Haskell. An example can be found in theory HOL-Library.Saturated.
Using "global_interpretation" in nested targets provides a way to
express the idea of »conditional interpretation« where the
interpretation depends on additional predicates which turn into explicit
assumptions after interpretation. A minimal example can be found in
theory HOL-ex.Interpretation_in_nested_targets.
Both generalizations emerged by appropriate generalization of the
existing local theory stack with minimal effort.
This refers to adb34395b622
Florian
OpenPGP_signature
Last updated: Jul 15 2022 at 23:21 UTC