[isabelle-dev] NEWS: Bundles for lattice syntax
makarius at sketis.net
Wed Sep 22 12:24:25 CEST 2021
*** HOL ***
* Theory HOL-Library.Lattice_Syntax has been superseded by bundle
"lattice_syntax": it can be used in a local context via 'include' or in
a global theory via 'unbundle'. The opposite declarations are bundled as
"no_lattice_syntax". Minor INCOMPATIBILITY.
This refers to Isabelle/cdf8952a86d5.
I have updated all earlier variations on it, including a few AFP entries. This
revealed a few diverging clones of old syntax. Now it is all standardized to
just one version, with very rare changes on the actual theory content. See
https://isabelle-dev.sketis.net/rAFPd12a1ce2753f with lemma maddux2d and lemma
More information about the isabelle-dev