src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
2014-10-30 haftmann 2014-10-30 more simp rules concerning dvd and even/odd
2014-10-24 hoelzl 2014-10-24 use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
2014-10-20 haftmann 2014-10-20 augmented and tuned facts on even/odd and division
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 ported Decision_Procs to new datatypes
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2014-03-18 wenzelm 2014-03-18 tuned proofs;
2014-03-18 wenzelm 2014-03-18 tuned proofs;
2014-03-13 nipkow 2014-03-13 enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
2014-03-12 wenzelm 2014-03-12 tuned proofs;
2014-03-10 wenzelm 2014-03-10 tuned proofs;
2014-03-09 wenzelm 2014-03-09 tuned proofs;
2014-03-08 wenzelm 2014-03-08 tuned proofs;
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-10-31 haftmann 2013-10-31 more convenient place for a theory in solitariness
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-07-30 wenzelm 2013-07-30 tuned proofs;
2013-07-15 wenzelm 2013-07-15 tuned specifications and proofs;
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