equal
deleted
inserted
replaced
135 *** HOL *** |
135 *** HOL *** |
136 |
136 |
137 * Theory HOL-Library.Lattice_Syntax has been superseded by bundle |
137 * Theory HOL-Library.Lattice_Syntax has been superseded by bundle |
138 "lattice_syntax": it can be used in a local context via 'include' or in |
138 "lattice_syntax": it can be used in a local context via 'include' or in |
139 a global theory via 'unbundle'. The opposite declarations are bundled as |
139 a global theory via 'unbundle'. The opposite declarations are bundled as |
140 "no_lattice_syntax". |
140 "no_lattice_syntax". Minor INCOMPATIBILITY. |
141 |
141 |
142 * Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone, |
142 * Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone, |
143 use explict expression instead. Minor INCOMPATIBILITY. |
143 use explict expression instead. Minor INCOMPATIBILITY. |
144 |
144 |
145 * Theory "HOL-Library.Multiset": consolidated abbreviations Mempty, |
145 * Theory "HOL-Library.Multiset": consolidated abbreviations Mempty, |