20 months ago immler 2017-10-24 generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
20 months ago haftmann 2017-10-20 added lemmas and tuned proofs
20 months ago haftmann 2017-10-09 tuned imports
20 months ago haftmann 2017-10-08 more fundamental definition of div and mod on int
2017-06-08 boehmes 2017-06-08 replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
2017-02-07 haftmann 2017-02-07 dropped superfluous preprocessing rule
2017-01-09 haftmann 2017-01-09 moved some lemmas to appropriate places
2017-01-03 paulson 2017-01-03 A few new lemmas and needed adaptations
2016-12-30 haftmann 2016-12-30 complete set of cases rules for integers known to be (non-)positive/negative; legacy theorem branding
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-10-03 haftmann 2016-10-03 more lemmas
2016-08-10 wenzelm 2016-08-10 misc tuning and modernization;
2016-08-10 nipkow 2016-08-10 "split add" -> "split"
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid improper use of "this";
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2016-02-17 haftmann 2016-02-17 generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
2016-01-11 eberlm 2016-01-11 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
2015-12-28 wenzelm 2015-12-28 prefer symbols for "abs";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-23 paulson 2015-11-23 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
2015-11-17 paulson 2015-11-17 Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-11-02 eberlm 2015-11-02 Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
2015-11-02 eberlm 2015-11-02 Rounding function, uniform limits, cotangent, binomial identities
2015-10-29 eberlm 2015-10-29 added many small lemmas about setsum/setprod/powr/...
2015-09-22 paulson 2015-09-22 New lemmas
2015-09-21 paulson 2015-09-21 new lemmas and movement of lemmas into place
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-08-31 wenzelm 2015-08-31 prefer symbols;
2015-08-08 haftmann 2015-08-08 direct bootstrap of integer division from natural division
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-06-25 haftmann 2015-06-25 more theorems
2015-04-30 paulson 2015-04-30 tidying some messy proofs
2015-03-10 paulson 2015-03-10 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
2015-03-05 paulson 2015-03-05 The function frac. Various lemmas about limits, series, the exp function, etc.
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-18 haftmann 2015-02-18 eliminated technical fact alias
2015-02-14 haftmann 2015-02-14 dropped redundancy
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-12 haftmann 2014-10-12 some more facts on divisibility
2014-10-12 haftmann 2014-10-12 generalized and consolidated some theorems concerning divisibility
2014-10-02 haftmann 2014-10-02 moved lemmas out of Int.thy which have nothing to do with int
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-05-07 hoelzl 2014-05-07 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
2014-04-10 kuncar 2014-04-10 simplify and fix theories thanks to 356a5efdb278
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-04 huffman 2014-03-04 remove simp rules made redundant by the replacement of neg_numeral with negated numerals
2014-02-12 blanchet 2014-02-12 transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well) * * * compile * * * tuned imports to prevent merge issues in 'Main'
2014-01-21 traytel 2014-01-21 removed theory dependency of BNF_LFP on Datatype
2014-01-20 blanchet 2014-01-20 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-04 haftmann 2013-11-04 streamlined setup of linear arithmetic