src/HOL/Library/Fundamental_Theorem_Algebra.thy
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-06-24 wenzelm 2015-06-24 tuned proofs -- less digits;
2015-06-22 wenzelm 2015-06-22 tuned proofs;
2015-06-13 wenzelm 2015-06-13 tuned proofs;
2015-06-13 wenzelm 2015-06-13 renamed "prems" to "that";
2015-06-10 wenzelm 2015-06-10 misc tuning;
2015-02-19 haftmann 2015-02-19 establish unique preferred fact names
2015-02-18 haftmann 2015-02-18 eliminated fact duplicates
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-08-05 wenzelm 2014-08-05 tuned proofs;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-05-07 hoelzl 2014-05-07 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
2014-04-29 wenzelm 2014-04-29 tuned proofs;
2014-04-28 wenzelm 2014-04-28 tuned proofs;
2014-04-28 wenzelm 2014-04-28 tuned proofs;
2014-04-12 nipkow 2014-04-12 made mult_pos_pos a simp rule
2014-04-04 blanchet 2014-04-04 tuned spaces
2014-02-25 paulson 2014-02-25 generalised some results using type classes
2014-02-25 paulson 2014-02-25 More complex-related lemmas
2014-02-07 paulson 2014-02-07 Simplified some proofs, deleting a lot of strange unused material at the end of the theory.
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-05 hoelzl 2013-11-05 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-08-18 wenzelm 2013-08-18 more symbols;
2013-06-15 haftmann 2013-06-15 lifting for primitive definitions; explicit conversions from and to lists of coefficients, used for generated code; replaced recursion operator poly_rec by fold_coeffs, preferring function definitions for non-trivial recursions; prefer pre-existing gcd operation for gcd
2013-03-26 wenzelm 2013-03-26 tuned proofs;
2013-03-26 wenzelm 2013-03-26 more standard imports;
2012-12-30 wenzelm 2012-12-30 uniform notation for == and \<equiv> (cf. 3e3c2af5e8a5);
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-01-17 huffman 2012-01-17 factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
2011-01-12 wenzelm 2011-01-12 eliminated global prems;
2010-07-19 haftmann 2010-07-19 diff_minus subsumes diff_def
2010-05-23 webertj 2010-05-23 Typo fixed.
2010-05-17 huffman 2010-05-17 simplify proof
2010-05-09 huffman 2010-05-09 avoid using real-specific versions of generic lemmas
2010-01-10 berghofe 2010-01-10 Adapted to changes in induct method.
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-08-31 nipkow 2009-08-31 tuned the simp rules for Int involving insert and intervals.
2009-05-28 huffman 2009-05-28 LIMSEQ_def -> LIMSEQ_iff
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-03-12 huffman 2009-03-12 remove trailing spaces
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-02 chaieb 2009-03-02 Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
2009-02-18 huffman 2009-02-18 move polynomial order stuff from Fundamental_Theorem_Algebra to Polynomial
2009-02-12 nipkow 2009-02-12 Moved FTA into Lib and cleaned it up a little.