HomeIsabelle/Phabricator
Theory_Data extend operation is obsolete and needs to be the identity function

ML

  • Theory_Data extend operation is obsolete and needs to be the identity function; merge should be conservative and not reset to the empty value. Subtle INCOMPATIBILITY and change of semantics (due to Theory.join_theory from Isabelle2020). Special extend/merge behaviour at the begin of a new theory can be achieved via Theory.at_begin.

This refers to Isabelle/efb7fd4a6d1f.

Written by makarius on Mon, Jul 20, 11:59 PM.
User
Projects
None
Subscribers
None

Event Timeline