*** 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 maddux2e. Makarius _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
