Theory_Data extend operation is obsolete and needs to be the identity function
- 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 Jul 20 2020, 11:59 PM.