src/HOL/Library/Univ_Poly.thy
2011-10-12 wenzelm 2011-10-12 tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-07-19 haftmann 2010-07-19 diff_minus subsumes diff_def
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-06-28 haftmann 2010-06-28 explicit is better than implicit
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
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-04-29 haftmann 2009-04-29 farewell to class recpower
2009-03-27 haftmann 2009-03-27 normalized imports
2009-03-12 huffman 2009-03-12 remove trailing spaces
2009-02-12 nipkow 2009-02-12 Moved FTA into Lib and cleaned it up a little.
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2009-01-16 haftmann 2009-01-16 moved Univ_Poly to Library
2008-11-17 haftmann 2008-11-17 tuned unfold_locales invocation
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-07-07 haftmann 2008-07-07 absolute imports of HOL/*.thy theories
2008-07-02 haftmann 2008-07-02 cleaned up some code generator configuration
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-03-17 wenzelm 2008-03-17 avoid rebinding of existing facts; removed duplicate lemmas;
2008-03-03 haftmann 2008-03-03 tuned
2008-02-25 chaieb 2008-02-25 A library for univariate polynomials -- generalizes old Hyperreal/Poly.thy from reals to locales