equal
deleted
inserted
replaced
160 it no longer fails on nested datatypes. Slight INCOMPATIBILITY. |
160 it no longer fails on nested datatypes. Slight INCOMPATIBILITY. |
161 |
161 |
162 * Session HOL-Algebra extended by additional lattice theory: the |
162 * Session HOL-Algebra extended by additional lattice theory: the |
163 Knaster-Tarski fixed point theorem and Galois Connections. |
163 Knaster-Tarski fixed point theorem and Galois Connections. |
164 |
164 |
165 * SMT module: The legacy module 'src/HOL/Library/Old_SMT.thy' has been removed. |
165 * SMT module: |
|
166 - The legacy module 'src/HOL/Library/Old_SMT.thy' has been removed. |
|
167 - Several small issues have been rectified in the 'smt' command. |
166 |
168 |
167 * Session HOL-Analysis: more material involving arcs, paths, covering |
169 * Session HOL-Analysis: more material involving arcs, paths, covering |
168 spaces, innessential maps, retracts. Major results include the Jordan |
170 spaces, innessential maps, retracts. Major results include the Jordan |
169 Curve Theorem and the Great Picard Theorem. |
171 Curve Theorem and the Great Picard Theorem. |
170 |
172 |