src/HOL/Algebra/UnivPoly.thy
2019-01-05 wenzelm isabelle update -u control_cartouches;
2018-09-24 nipkow Prefix form of infix with * on either side no longer needs special treatment
2018-06-14 paulson reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
2018-02-15 wenzelm more symbols;
2018-01-10 nipkow ran isabelle update_op on all sources
2018-01-10 nipkow tuned op's
2018-01-05 nipkow Renamed (^) to [^] in preparation of the move from "op X" to (X)
2017-11-26 wenzelm more symbols;
2017-01-17 wenzelm more symbols;
2016-09-16 wenzelm more symbols;
2016-05-26 wenzelm isabelle update_cartouches -c -t;
2015-11-04 ballarin Qualifiers in locale expressions default to mandatory regardless of the command.
2015-10-27 paulson Cauchy's integral formula, required lemmas, and a bit of reorganisation
2015-10-10 wenzelm prefer symbols;
2015-10-10 wenzelm isabelle update_cartouches;
2015-09-13 wenzelm tuned proofs -- less legacy;
2015-04-17 Rene Thiemann finprod takes 1 in case of infinite sets => remove several "finite A" assumptions
2014-10-07 wenzelm more antiquotations;
2014-08-05 wenzelm tuned proofs -- fewer warnings;
2014-07-04 haftmann reduced name variants for assoc and commute on plus and mult
2014-03-05 wenzelm more symbols;
2013-12-25 haftmann prefer more canonical names for lemmas on min/max
2012-10-19 webertj Renamed {left,right}_distrib to distrib_{right,left}.
2011-09-12 nipkow new fastforce replacing fastsimp - less confusing name
2011-09-07 huffman avoid using legacy theorem names
2011-09-02 wenzelm tuned proofs;
2010-08-02 ballarin Revised proof of long division contributed by Jesus Aransay.
2010-04-07 ballarin Merged resolving conflicts NEWS and locale.ML.
2010-02-15 ballarin Tuned interpretation proofs.
2010-03-21 wenzelm standard headers;
2010-03-21 wenzelm slightly more uniform definitions -- eliminated old-style meta-equality;
2010-01-10 berghofe Adapted to changes in induct method.
2009-11-13 nipkow renamed lemmas "anti_sym" -> "antisym"
2009-10-17 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
2009-08-31 nipkow tuned the simp rules for Int involving insert and intervals.
2009-08-28 nipkow Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
2009-03-26 wenzelm interpretation/interpret: prefixes are mandatory by default;
2009-03-08 wenzelm proper local context for text with antiquotations;
2008-12-19 ballarin More porting to new locales.
2008-12-17 ballarin More porting to new locales.
2008-12-16 ballarin More porting to new locales.
2008-11-17 haftmann tuned unfold_locales invocation
2008-08-18 ballarin Theorem on polynomial division and lemmas.
2008-08-01 ballarin Generalised polynomial lemmas from cring to ring.
2008-07-31 ballarin Tuned (for the sake of a meaningless log entry).
2008-07-15 ballarin Removed uses of context element includes.
2008-05-17 wenzelm avoid undeclared variables within proofs;
2008-03-05 wenzelm explicit referencing of background facts;
2007-06-12 wenzelm tuned proofs: avoid implicit prems;
2007-05-10 wenzelm tuned proofs;
2006-11-23 wenzelm prefer antiquotations over LaTeX macros;
2006-08-30 webertj lin_arith_prover: splitting reverted because of performance loss
2006-08-03 ballarin Restructured algebra library, added ideals and quotient rings.
2006-08-02 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-07-26 webertj linear arithmetic splits certain operators (e.g. min, max, abs)
2006-07-04 ballarin Method intro_locales replaced by intro_locales and unfold_locales.
2006-06-20 ballarin Restructured locales with predicates: import is now an interpretation.
2006-06-06 ballarin Improved parameter management of locales.
2006-05-05 wenzelm get rid of 'concl is';
2005-08-17 ballarin Use interpretation in locales.
2005-07-01 berghofe Removed setsubgoaler hack (thanks to strengthened finsum_cong).
2005-06-17 haftmann migrated theory headers to new format
2005-05-09 paulson from simplesubst to new subst
2005-04-18 ballarin Interpretation supports statically scoped attributes; documentation.
2005-04-11 ballarin First release of interpretation commands.
2005-03-09 ballarin First version of global registration command.
2005-02-01 paulson the new subst tactic, by Lucas Dixon
2004-08-02 ballarin Theories now take advantage of recent syntax improvements with (structure).
2004-07-26 ballarin New prover for transitive and reflexive-transitive closure of relations.
2004-07-15 nipkow Moved to new m<..<n syntax for set intervals.
2004-06-17 paulson removal of magmas and semigroups
2004-05-06 wenzelm tuned document;
2004-04-23 wenzelm improved notation;
2004-04-22 wenzelm improved notation;
2004-04-16 wenzelm simplified ML code for setsubgoaler;
2004-04-16 wenzelm tuned document;
2004-04-13 ballarin Added brief intro text.
2004-02-19 ballarin New lemmas about inversion of restricted functions.
2003-05-07 ballarin Small changes for release Isabelle 2003.
2003-05-02 ballarin HOL-Algebra complete for release Isabelle2003 (modulo section headers).
2003-04-30 ballarin HOL-Algebra: New polynomial development added.
less more (0) tip