src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
2011-02-21 krauss 2011-02-21 recdef -> fun; curried
2011-02-21 krauss 2011-02-21 strengthened polymul.induct
2011-02-21 krauss 2011-02-21 dropped stupid name
2011-02-21 krauss 2011-02-21 recdef -> function
2011-02-21 wenzelm 2011-02-21 tuned proofs -- eliminated prems;
2011-02-14 krauss 2011-02-14 strengthened induction rule; clarified some proofs
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-12-25 krauss 2010-12-25 dropped duplicate unused lemmas; spelling
2010-12-25 krauss 2010-12-25 partial_function (tailrec) replaces function (tailrec); dropped unnecessary domain reasoning; curried polydivide_aux
2010-09-08 haftmann 2010-09-08 modernized primrec
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 class division_ring_inverse_zero
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-08 wenzelm 2010-02-08 modernized some syntax translations;
2010-02-08 haftmann 2010-02-08 tuned header
2010-01-10 berghofe 2010-01-10 Adapted to changes in induct method.
2009-10-28 wenzelm 2009-10-28 eliminated hard tabulators, guessing at each author's individual tab-width;
2009-10-25 chaieb 2009-10-25 Multivariate polynomials library over fields