src/HOL/Algebra/abstract/Ideal.ML
2002-11-28 ballarin 2002-11-28 HOL-Algebra partially ported to Isar.
2002-10-18 nipkow 2002-10-18 Mod due to: Added a few thms about UN/INT/{}/UNIV
2001-06-26 paulson 2001-06-26 resolved name clash
2001-02-10 ballarin 2001-02-10 Changes to HOL/Algebra: - Axclasses consolidated (axiom one_not_zero). - Now uses summation operator setsum; SUM has been removed. - Priority of infix assoc changed to 50, in accordance to dvd.
2001-01-09 nipkow 2001-01-09 `` -> ` and ``` -> ``
2001-01-05 nipkow 2001-01-05 Changed priority of dvd from 70 to 50 as befits a relation.
2000-10-17 paulson 2000-10-17 tidying and renaming of contrapos rules
2000-10-12 paulson 2000-10-12 tidied
2000-04-13 paulson 2000-04-13 tidied
1999-11-05 paulson 1999-11-05 Algebra and Polynomial theories, by Clemens Ballarin