src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
2012-11-29 wenzelm 2012-11-29 more robust syntax that survives collapse of \<^isub> and \<^sub>;
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-03-17 wenzelm 2012-03-17 tuned proofs;
2011-10-12 wenzelm 2011-10-12 tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
2011-02-25 nipkow 2011-02-25 added simp lemma nth_Cons_pos to List
2011-02-21 wenzelm 2011-02-21 merged, resolving spurious conflicts and giving up Reflected_Multivariate_Polynomial.thy from ab5d2d81f9fb;
2011-02-21 krauss 2011-02-21 eliminated global prems
2011-02-21 krauss 2011-02-21 modernized specification; curried
2011-02-21 krauss 2011-02-21 recdef -> fun; curried
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