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
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-10-31 haftmann 2013-10-31 restructed
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-09-16 kuncar 2013-09-16 use lifting_forget for deregistering numeric types as a quotient type
2013-08-18 haftmann 2013-08-18 added lemma
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-05-15 kuncar 2013-05-15 stronger reflexivity prover
2013-02-20 hoelzl 2013-02-20 split dense into inner_dense_order and no_top/no_bot
2013-02-19 kuncar 2013-02-19 delete also predicates on relations when hiding an implementation of an abstract type
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2013-02-14 haftmann 2013-02-14 abandoned theory Plain
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-06-02 huffman 2012-06-02 transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
2012-05-30 huffman 2012-05-30 convert Int.thy to use lifting and transfer
2012-05-30 huffman 2012-05-30 remove unnecessary simp rules involving Abs_Integ
2012-04-01 huffman 2012-04-01 removed Nat_Numeral.thy, moving all theorems elsewhere
2012-03-30 huffman 2012-03-30 load Tools/numeral.ML in Num.thy
2012-03-30 huffman 2012-03-30 set up numeral reorient simproc in Num.thy
2012-03-30 huffman 2012-03-30 move lemmas from Nat_Numeral to Int.thy and Num.thy
2012-03-29 huffman 2012-03-29 move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-02 bulwahn 2012-03-02 adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
2011-12-29 haftmann 2011-12-29 semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat; attribute code_abbrev superseedes code_unfold_post
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-11-17 huffman 2011-11-17 simplify some proofs
2011-11-17 huffman 2011-11-17 Int.thy: remove duplicate lemmas double_less_0_iff and odd_less_0, use {even,odd}_less_0_iff instead
2011-10-20 huffman 2011-10-20 removed mult_Bit1 from int_arith_rules (cf. 882403378a41 and 3078fd2eec7b, where mult_num1 erroneously replaced mult_1)
2011-10-19 wenzelm 2011-10-19 inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);
2011-10-19 bulwahn 2011-10-19 removing old code generator setup for integers
2011-10-09 huffman 2011-10-09 Int.thy: discontinued some legacy theorems
2011-09-04 huffman 2011-09-04 introduce abbreviation 'int' earlier in Int.thy
2011-09-04 huffman 2011-09-04 move lemmas nat_le_iff and nat_mono into Int.thy
2011-09-03 huffman 2011-09-03 remove duplicate lemma nat_zero in favor of nat_0