src/HOL/ZF/LProd.thy
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-03-01 wenzelm 2010-03-01 tuned final whitespace;
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
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.