src/HOL/Algebra/poly/LongDiv.thy
2010-09-06 wenzelm 2010-09-06 more antiquotations;
2010-03-21 wenzelm 2010-03-21 standard headers;
2009-04-23 haftmann 2009-04-23 adaptions due to rearrangment of power operation
2008-06-14 wenzelm 2008-06-14 tuned proof;
2008-03-19 wenzelm 2008-03-19 more antiquotations;
2007-09-27 paulson 2007-09-27 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering theorems of Nat.thy are hidden by the Ordering.thy versions
2007-03-02 haftmann 2007-03-02 prefix of class interpretation not mandatory any longer
2006-11-19 wenzelm 2006-11-19 HOL-Algebra: converted legacy ML scripts;
2005-09-06 wenzelm 2005-09-06 axclass: name space prefix is now "c_class" instead of just "c";
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2004-05-10 obua 2004-05-10 moved first lemma in LongDiv.ML to LongDiv.thy
2002-11-28 ballarin 2002-11-28 HOL-Algebra partially ported to Isar.
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.
1999-11-05 paulson 1999-11-05 Algebra and Polynomial theories, by Clemens Ballarin