| Tue, 10 Oct 2017 17:15:37 +0100 | paulson | Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems | file | diff | annotate |
| Tue, 19 Sep 2017 16:37:19 +0100 | paulson | Using the "constant_on" operator | file | diff | annotate |
| Thu, 17 Aug 2017 14:52:56 +0200 | eberlm | Replaced subseq with strict_mono | file | diff | annotate |
| Sun, 14 May 2017 15:35:25 +0200 | wenzelm | eliminated suspicious Unicode; | file | diff | annotate |
| Thu, 16 Mar 2017 16:02:18 +0000 | paulson | Removed [simp] status for Complex_eq. Also tidied some proofs | file | diff | annotate |
| Tue, 28 Feb 2017 13:51:47 +0000 | paulson | Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands | file | diff | annotate |
| Wed, 22 Feb 2017 16:21:26 +0000 | paulson | The Great Picard Theorem | file | diff | annotate |