src/HOL/Library/Fundamental_Theorem_Algebra.thy
 2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}. file | diff | annotate 2012-01-17 huffman 2012-01-17 factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero file | diff | annotate 2011-01-12 wenzelm 2011-01-12 eliminated global prems; file | diff | annotate 2010-07-19 haftmann 2010-07-19 diff_minus subsumes diff_def file | diff | annotate 2010-05-23 webertj 2010-05-23 Typo fixed. file | diff | annotate 2010-05-17 huffman 2010-05-17 simplify proof file | diff | annotate 2010-05-09 huffman 2010-05-09 avoid using real-specific versions of generic lemmas file | diff | annotate 2010-01-10 berghofe 2010-01-10 Adapted to changes in induct method. file | diff | annotate 2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers; file | diff | annotate 2009-08-31 nipkow 2009-08-31 tuned the simp rules for Int involving insert and intervals. file | diff | annotate 2009-05-28 huffman 2009-05-28 LIMSEQ_def -> LIMSEQ_iff file | diff | annotate 2009-04-29 haftmann 2009-04-29 farewell to class recpower file | diff | annotate 2009-03-12 huffman 2009-03-12 remove trailing spaces file | diff | annotate 2009-03-04 blanchet 2009-03-04 Merge. file | diff | annotate 2009-03-04 blanchet 2009-03-04 Merge. file | diff | annotate 2009-03-02 chaieb 2009-03-02 Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy file | diff | annotate 2009-02-18 huffman 2009-02-18 move polynomial order stuff from Fundamental_Theorem_Algebra to Polynomial file | diff | annotate 2009-02-12 nipkow 2009-02-12 Moved FTA into Lib and cleaned it up a little. file | diff | annotate | base