src/HOL/Algebra/IntRing.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-07-01 paulson new lemmas, de-applying, etc.
2018-06-06 paulson resolution of name clashes in Algebra
2018-01-16 wenzelm standardized towards new-style formal comments: isabelle update_comments;
2018-01-10 nipkow ran isabelle update_op on all sources
2018-01-10 nipkow tuned op's
2018-01-06 nipkow tuned op
2017-12-02 haftmann more simplification rules
2017-11-26 wenzelm more symbols;
2017-11-04 wenzelm prefer main entry points of HOL;
2017-08-18 wenzelm session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2017-04-06 haftmann session containing computational algebra
2016-10-17 nipkow setprod -> prod
2016-10-17 nipkow setsum -> sum
2016-10-16 haftmann eliminated irregular aliasses
2016-08-08 eberlm is_prime -> prime
2016-07-21 eberlm Overhaul of prime/multiplicity/prime_factors
2016-05-26 wenzelm isabelle update_cartouches -c -t;
2016-02-17 haftmann dropped various legacy fact bindings
2015-12-28 wenzelm more symbols;
2015-11-04 ballarin Keyword 'rewrites' identifies rewrite morphisms.
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-07-05 haftmann prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann reduced name variants for assoc and commute on plus and mult
2014-03-07 wenzelm tuned proofs;
2014-03-05 wenzelm more symbols;
2014-02-02 paulson Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
2014-01-27 paulson converting to new Number_Theory
2012-10-19 webertj Renamed {left,right}_distrib to distrib_{right,left}.
2011-09-07 huffman avoid using legacy theorem names
2011-09-02 wenzelm tuned proofs;
2011-01-06 ballarin Abelian group facts obtained from group facts via interpretation (sublocale).
2010-03-21 wenzelm standard headers;
2010-03-21 wenzelm slightly more uniform definitions -- eliminated old-style meta-equality;
2010-03-01 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2009-11-13 nipkow moved lemma from Algebra/IntRing to Ring_and_Field
2009-11-13 nipkow renamed lemmas "anti_sym" -> "antisym"
2009-09-01 haftmann some reorganization of number theory
2009-03-26 wenzelm interpretation/interpret: prefixes are mandatory by default;
2009-02-17 nipkow Cleaned up IntDiv and removed subsumed lemmas.
2009-01-31 nipkow added some simp rules
2009-01-10 wenzelm fixed proof involving dvd;
2008-12-19 ballarin More porting to new locales
2008-12-16 ballarin More porting to new locales.
2008-11-17 haftmann tuned unfold_locales invocation
2008-10-07 haftmann arbitrary is undefined
2008-09-02 ballarin Interpretation commands no longer accept interpretation attributes.
2008-08-01 ballarin Generalised polynomial lemmas from cring to ring.
2008-07-30 ballarin New locales for orders and lattices where the equivalence relation is not restricted to equality.
2008-01-15 haftmann joined theories IntDef, Numeral, IntArith to theory Int
2007-08-02 ballarin Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
2007-07-24 ballarin Interpretation of rings (as integers) maps defined operations to defined
2007-01-12 ballarin Reverted to structure representation with records.
2006-12-22 ballarin Experimenting with interpretations of "definition".
2006-10-16 ballarin Order and lattice structures no longer based on records.
2006-08-03 ballarin Restructured algebra library, added ideals and quotient rings.
less more (0) tip