2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2007-07-11 berghofe 2007-07-11 Restored set notation in Multiset theory.
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-02-07 berghofe 2007-02-07 - Adapted to new inductive definition package - Adapted to changes in Multiset theory
2006-06-05 krauss 2006-06-05 Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure". This simplifies some proofs.
2006-03-07 obua 2006-03-07 Added HOL-ZF to Isabelle.