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.
- Projects
- None
- Subscribers
- None