2010-03-01 ago replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2009-10-22 ago inv_onto -> inv_into
2009-10-18 ago merged
2009-10-18 ago Inv -> inv_onto, inv abbr. inv_onto UNIV.
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2009-06-22 ago tuned FuncSet
2009-06-19 ago Made Pi_I [simp]
2009-03-26 ago interpretation/interpret: prefixes are mandatory by default;
2008-12-17 ago More porting to new locales.
2008-12-16 ago More porting to new locales.
2008-11-17 ago tuned unfold_locales invocation
2008-07-31 ago Tuned (for the sake of a meaningless log entry).
2008-07-30 ago New locales for orders and lattices where the equivalence relation is not restricted to equality.
2008-07-29 ago Unit_inv_l, Unit_inv_r made [simp].
2008-07-15 ago Removed uses of context element includes.
2008-05-07 ago Replaced forward proofs of existential statements by backward proofs
2008-03-05 ago explicit referencing of background facts;
2007-06-13 ago tuned proofs: avoid implicit prems;
2007-01-12 ago Reverted to structure representation with records.
2006-10-16 ago Order and lattice structures no longer based on records.
2006-08-03 ago Restructured algebra library, added ideals and quotient rings.
2006-07-04 ago Method intro_locales replaced by intro_locales and unfold_locales.
2006-07-04 ago Minor new lemmas.
2006-06-20 ago Restructured locales with predicates: import is now an interpretation.
2006-06-06 ago Improved parameter management of locales.
2006-05-22 ago removed unchecked'';
2006-05-20 ago pow: unchecked;
2005-06-17 ago migrated theory headers to new format
2005-04-18 ago Interpretation supports statically scoped attributes; documentation.
2005-04-11 ago First release of interpretation commands.
2004-07-26 ago New prover for transitive and reflexive-transitive closure of relations.
2004-06-17 ago removal of magmas and semigroups
2004-06-01 ago tidied
2004-05-26 ago more group isomorphisms
2004-05-19 ago more results about isomorphisms
2004-05-14 ago Change of theory hierarchy: Group is now based in Lattice.
2004-05-06 ago tuned document;
2004-05-01 ago improved syntax;
2004-04-22 ago improved notation;
2004-04-13 ago Various changes to HOL-Algebra;
2003-12-10 ago New structure "partial_object" as common root for lattices and magmas.
2003-11-06 ago Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
2003-05-07 ago Small changes for release Isabelle 2003.
2003-05-02 ago HOL-Algebra complete for release Isabelle2003 (modulo section headers).
2003-05-01 ago new proofs about direct products, etc.
2003-05-01 ago moving Bij.thy from GroupTheory to Algebra
2003-04-30 ago HOL-Algebra: New polynomial development added.
2003-04-30 ago Greatly extended CRing. Added Module.
2003-03-10 ago First distributed version of Group and Ring theory.
2003-02-27 ago Change to meta simplifier: congruence rules may now have frees as head of term.
2003-02-14 ago Product operator added --- preliminary.
2003-02-10 ago New development of algebra: Groups.