| Wed, 09 Oct 2019 14:51:54 +0000 | haftmann | dedicated fact collections for algebraic simplification rules potentially splitting goals | file | diff | annotate |
| Tue, 08 Oct 2019 10:26:40 +0000 | haftmann | formally augmented corresponding rules for field_simps | file | diff | annotate |
| Thu, 26 Sep 2019 12:24:02 +0100 | paulson | A little more material from the Fourier AFP entry, and the correction of two very slow proof lines | file | diff | annotate |
| Tue, 17 Sep 2019 12:36:04 +0100 | paulson | A few new theorems, tidying up and deletion of obsolete material | file | diff | annotate |
| Mon, 16 Sep 2019 17:03:13 +0100 | paulson | A little-known material, and some tidying up | file | diff | annotate |
| Fri, 13 Sep 2019 12:46:36 +0100 | paulson | New theory Equivalence_Measurable_On_Borel, with the HOL Light notion of measurable_on and its equivalence to ours | file | diff | annotate |