241 http://isabelle.in.tum.de/Bali/); |
241 http://isabelle.in.tum.de/Bali/); |
242 |
242 |
243 * HOL/Algebra: new theory of rings and univariate polynomials, by |
243 * HOL/Algebra: new theory of rings and univariate polynomials, by |
244 Clemens Ballarin; |
244 Clemens Ballarin; |
245 |
245 |
246 * HOL/NumberTheory: Fundamental Theorem of Arithmetic, Chinese |
246 * HOL/NumberTheory: fundamental Theorem of Arithmetic, Chinese |
247 Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, by Thomas M |
247 Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, by Thomas M |
248 Rasmussen; |
248 Rasmussen; |
|
249 |
|
250 * HOL/Lattice: fundamental concepts of lattice theory and order |
|
251 structures, including duals, properties of bounds versus algebraic |
|
252 laws, lattice operations versus set-theoretic ones, the Knaster-Tarski |
|
253 Theorem for complete lattices etc.; may also serve as a demonstration |
|
254 for abstract algebraic reasoning using axiomatic type classes, and |
|
255 mathematics-style proof in Isabelle/Isar; by Markus Wenzel; |
249 |
256 |
250 * HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog, by David |
257 * HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog, by David |
251 von Oheimb; |
258 von Oheimb; |
252 |
259 |
253 * HOL/Lambda: converted into new-style theory and document; |
260 * HOL/Lambda: converted into new-style theory and document; |