Page MenuHomeIsabelle/Phabricator

Localized record package
Open, NormalPublic


The Isabelle/HOL record package is a leftover from ancient global-theory specification era. It should be properly localized, but this is difficult due to special features that have accumulated over time; some are required in special applications, some might be superfluous.

It will require substantial research and development to sort this out.

Event Timeline

makarius triaged this task as Normal priority.Feb 19 2020, 8:48 PM
makarius created this task.