src/HOL/Parity.thy
22 months ago haftmann 2017-10-09 canonical multiplicative euclidean size
22 months ago haftmann 2017-10-09 clarified parity
22 months ago haftmann 2017-10-08 more fundamental definition of div and mod on int
22 months ago haftmann 2017-10-08 one uniform type class for parity structures
22 months ago haftmann 2017-10-08 elementary definition of division on natural numbers
24 months ago bulwahn 2017-08-27 another fact on (- 1) ^ _
2017-01-04 haftmann 2017-01-04 moved euclidean ring to HOL
2016-08-10 wenzelm 2016-08-10 misc tuning and modernization;
2016-03-12 haftmann 2016-03-12 model characters directly as range 0..255 * * * operate on syntax terms rather than asts
2016-01-06 hoelzl 2016-01-06 add the proof of the central limit theorem
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-02 eberlm 2015-11-02 Rounding function, uniform limits, cotangent, binomial identities
2015-08-06 haftmann 2015-08-06 slight cleanup of lemmas
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-06-23 paulson 2015-06-23 Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
2015-06-01 haftmann 2015-06-01 correct sort constraints for abbreviations in type classes * * * yet another bunch of corrections
2015-03-23 haftmann 2015-03-23 distributivity of partial minus establishes desired properties of dvd in semirings
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-26 haftmann 2014-10-26 eliminated redundancies; more simp rules
2014-10-23 haftmann 2014-10-23 even further downshift of theory Parity in the hierarchy
2014-10-23 haftmann 2014-10-23 further downshift of theory Parity in the hierarchy
2014-10-23 haftmann 2014-10-23 slight generalization and unification of simp rules for algebraic procedures
2014-10-23 haftmann 2014-10-23 downshift of theory Parity in the hierarchy
2014-10-23 haftmann 2014-10-23 parity induction over natural numbers
2014-10-21 haftmann 2014-10-21 turn even into an abbreviation
2014-10-20 wenzelm 2014-10-20 repared document;
2014-10-20 haftmann 2014-10-20 more standard declaration for presburger
2014-10-20 haftmann 2014-10-20 augmented and tuned facts on even/odd and division
2014-10-19 haftmann 2014-10-19 prefer generic elimination rules for even/odd over specialized unfold rules for nat
2014-10-16 haftmann 2014-10-16 tuned
2014-10-16 haftmann 2014-10-16 standard elimination rule for even
2014-10-16 haftmann 2014-10-16 tuned facts on even and power
2014-10-16 haftmann 2014-10-16 restructured
2014-10-16 haftmann 2014-10-16 even more cleanup
2014-10-14 haftmann 2014-10-14 legacy cleanup
2014-10-14 haftmann 2014-10-14 more algebraic deductions for facts on even/odd
2014-10-14 haftmann 2014-10-14 more algebraic deductions for facts on even/odd
2014-10-14 haftmann 2014-10-14 purely algebraic characterization of even and odd
2014-10-09 haftmann 2014-10-09 more foundational definition for predicate even
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-10-31 haftmann 2013-10-31 purely algebraic foundation for even/odd
2013-10-31 haftmann 2013-10-31 moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas; tuned presburger
2012-03-30 huffman 2012-03-30 remove redundant simp rule
2012-03-30 huffman 2012-03-30 add simp rules for eve/odd on numerals
2012-03-27 huffman 2012-03-27 remove redundant lemma
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-05-11 huffman 2010-05-11 fix duplicate simp rule warning
2010-05-06 haftmann 2010-05-06 tuned proof
2010-03-08 haftmann 2010-03-08 transfer: avoid camel case
2010-03-06 huffman 2010-03-06 generalize some lemmas from class linordered_ring_strict to linordered_ring
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-02-08 haftmann 2010-02-08 dropped accidental duplication of "lin" prefix from cs. 108662d50512
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-10-30 haftmann 2009-10-30 moved some div/mod lemmas to theory Divides
2009-10-29 haftmann 2009-10-29 moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-06-19 nipkow 2009-06-19 fixed thm name
2009-05-14 nipkow 2009-05-14 Cleaned up Parity a little
2009-04-28 haftmann 2009-04-28 stripped class recpower further