Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS


view this post on Zulip Email Gateway (Oct 29 2020 at 13:49):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

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

view this post on Zulip 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: Mar 04 2024 at 10:08 UTC