2004-04-13 ballarin 2004-04-13 Various changes to HOL-Algebra; Locale instantiation.
2004-02-19 ballarin 2004-02-19 New lemmas about inversion of restricted functions. HOL-Algebra: new locale "ring" for non-commutative rings.
2003-12-10 ballarin 2003-12-10 New structure "partial_object" as common root for lattices and magmas.
2003-09-30 ballarin 2003-09-30 Changed order of prems in finprod_cong. Slight speedup.
2003-04-30 ballarin 2003-04-30 Greatly extended CRing. Added Module.
2003-04-01 ballarin 2003-04-01 Fixed Coset.thy (proved theorem factorgroup_is_group).
2003-03-14 ballarin 2003-03-14 Bugs fixed and operators finprod and finsum.
2003-03-10 ballarin 2003-03-10 First distributed version of Group and Ring theory.
2003-02-27 ballarin 2003-02-27 Change to meta simplifier: congruence rules may now have frees as head of term.