src/HOL/Hyperreal/Poly.thy
2007-10-20 chaieb 2007-10-20 fixed proofs
2007-09-27 paulson 2007-09-27 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering theorems of Nat.thy are hidden by the Ordering.thy versions
2007-06-25 nipkow 2007-06-25 removed redundant lemma
2007-06-11 chaieb 2007-06-11 tuned Proof
2007-06-07 huffman 2007-06-07 tuned
2007-06-05 chaieb 2007-06-05 Polynomials now only depend on Deriv; Definition of degree changed
2007-05-16 huffman 2007-05-16 minimize imports
2007-04-26 wenzelm 2007-04-26 eliminated unnamed infixes, tuned syntax;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-10-09 wenzelm 2006-10-09 attribute symmetric: zero_var_indexes;
2006-09-30 huffman 2006-09-30 add type annotations for DERIV
2006-08-30 webertj 2006-08-30 lin_arith_prover: splitting reverted because of performance loss
2006-07-30 webertj 2006-07-30 lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-06-02 wenzelm 2006-06-02 misc cleanup;
2006-01-05 wenzelm 2006-01-05 replaced swap by contrapos_np;
2005-09-28 paulson 2005-09-28 new lemma
2005-07-29 avigad 2005-07-29 changed import to Ln
2005-07-27 paulson 2005-07-27 removed the dependence on abs_mult
2005-02-21 nipkow 2005-02-21 comprehensive cleanup, replacing sumr by setsum
2004-10-19 paulson 2004-10-19 converted some induct_tac to induct
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-03-05 paulson 2004-03-05 Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal
2001-11-16 paulson 2001-11-16 even more theories from Jacques