equal
deleted
inserted
replaced
241 of Formal power series. |
241 of Formal power series. |
242 |
242 |
243 * Session HOL-Number_Theory: More material on residue rings in |
243 * Session HOL-Number_Theory: More material on residue rings in |
244 Carmichael's function, primitive roots, more properties for "ord". |
244 Carmichael's function, primitive roots, more properties for "ord". |
245 |
245 |
246 * Session HOL-Analysis: Better organization and much more material, |
246 * Session HOL-Homology: New, a port of HOL Light's homology library, |
247 including algebraic topology. |
247 with new proofs of "invariance of domain" and related results. |
248 |
248 |
249 * Session HOL-Algebra: Much more material on group theory. |
249 * Session HOL-Analysis: Better organization and much more material |
|
250 at the level of abstract topological spaces. |
|
251 |
|
252 * Session HOL-Algebra: Much more material on group theory, mostly ported |
|
253 from HOL Light. |
250 |
254 |
251 * Session HOL-SPARK: .prv files are no longer written to the |
255 * Session HOL-SPARK: .prv files are no longer written to the |
252 file-system, but exported to the session database. Results may be |
256 file-system, but exported to the session database. Results may be |
253 retrieved via "isabelle build -e HOL-SPARK-Examples" on the |
257 retrieved via "isabelle build -e HOL-SPARK-Examples" on the |
254 command-line. |
258 command-line. |