diff options
| -rw-r--r-- | etc/ChangeLog | 80 |
1 files changed, 80 insertions, 0 deletions
diff --git a/etc/ChangeLog b/etc/ChangeLog new file mode 100644 index 0000000..f13548b --- /dev/null +++ b/etc/ChangeLog @@ -0,0 +1,80 @@ +24/11/2015 - major reorganization of the archive - version 1.6 + * Files split into subdirectories: ssreflect, algebra, fingroup, + solvable, field and character. + + * The archive is now open and based on git. Public mirror at: + https://github.com/math-comp/math-comp + + * Renamings or replacements: + conjC_closed -> cfConjC_closed + class_transr -> class_eqP + cfclass_transl -> cfclass_transr + nontrivial_ideal -> proper_ideal + zchar_orthonormalP -> vchar_orthonormalP + + * Statements that changed: + orbit_in_transl, orbit_sym, orbit_trans, orbit_transl, orbit_transr, + cfAut_char, cfConjC_char, invg_lcosets, lcoset_transl, + lcoset_transr, rcoset_transl, rcoset_transr, mem2_last, + bind_unless, unless_contra, all_and2, all_and3, all_and4, all_and5, + ltr0_neq0, ltr_prod, Zisometry_of_iso + + * New theorems: + orbit_in_eqP, cards_draws, cfAut_lin_char, cfConjC_lin_char, + extend_cfConjC_subset, isometry_of_free, cfAutK, cfAutVK, + lcoset_eqP, rcoset_eqP, class_eqP, gFsub_trans, gFnorms, + gFchar_trans, gFnormal_trans, gFnorm_trans, mem2_seq1, + dvdn_fact, prime_above, subKr, subrI, subIr, subr0_eq, + divrI, divIr, divKr, divfI, divIf, divKf, impliesP, impliesPn, + unlessL, unlessR, unless_sym, unlessP (coercion), classicW, + ltr_prod_nat + + * New notation: "\unless C, P" + +12/03/2014 - split the archive in SSReflect and MathComp - version 1.5 + * With this release "ssreflect" has been split into two packages. + The Ssreflect one contains the proof language (plugin for Coq) and a + small set of core theory libraries about boolean, natural numbers, + sequences, decidable equality and finite types. The Mathematical + Components one contains advanced theory files covering a wider + spectrum of mathematics. + + * With respect to version 1.4 the proof language got a few new + features related to forward reasoning and some bugfixes. The + Mathematical Components library features 16 new theory files and in + particular: some field and Galois theory, advanced character theory + and a construction of algebraic numbers. + +05/09/2012 - ssreflect - version 1.4 + * With this release the plugin code received many bug fixes and the + existing libraries relevant updates. This release also includes + some new libraries on the following topics: rational numbers, + divisibility of integers, F-algebras, finite dimensional field + extensions and Euclidean division for polynomials over a ring. + + * The release includes a major code refactoring of the plugin for Coq + 8.4. In particular a documented ML API to access the pattern matching + facilities of Ssreflect from third party plugins has been introduced. + +14/03/2011 - ssreflect - version 1.3 + * The tactic language has been extended with several new features, + inspired by the five years of intensive use in our project. However we + have kept the core of the language unchanged; the new library compiles + with Ssreflect 1.2. Users of a Coq 8.2 toplevel statically linked + with Ssreflect 1.2 need to comment the Declare ML Module "ssreflect" + line in ssreflect.v to properly compile the 1.3 library. We will + continue supporting new releases of Coq in due course. + + * The new library adds general linear algebra (matrix rank, subspaces) + and all of the advanced finite group that was developed in the course + of completing the Local Analysis part of the Odd Order Theorem, + starting from the Sylow and Hall theorems and including full structure + theorems for abelian, extremal and extraspecial groups, and general + (modular) linear representation theory. + +14/08/2009 - ssreflect - version 1.2 + * No change log + +18/03/2008 - ssreflect - version 1.1 + * First public release + |