[isabelle-dev] NEWS

[Florian Haftmann]

"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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20210616/823c510c/attachment.sig>