src/HOL/Num.thy
2014-09-21 haftmann 2014-09-21 explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-09-11 blanchet 2014-09-11 updated news
2014-09-03 blanchet 2014-09-03 tuned imports
2014-09-03 blanchet 2014-09-03 use 'datatype_new' in 'Main'
2014-09-01 blanchet 2014-09-01 renamed BNF theories
2014-09-01 blanchet 2014-09-01 renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-03-07 wenzelm 2014-03-07 more official const syntax: avoid educated guessing by Syntax_Phases.decode_term;
2014-02-17 blanchet 2014-02-17 renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
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-08-18 haftmann 2013-08-18 generalized sort constraint of lemmas
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-28 wenzelm 2013-05-28 more explicit Printer.type_emphasis, depending on show_type_emphasis; tuned signature;
2013-05-27 wenzelm 2013-05-27 tuned;
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
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-01-11 haftmann 2013-01-11 sharing of recursive results on evaluation
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-03 wenzelm 2012-10-03 more explicit show_type_constraint, show_sort_constraint;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-02 huffman 2012-04-02 remove unnecessary qualifiers on names
2012-04-02 huffman 2012-04-02 add lemma Suc_1
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 tuned proof
2012-03-30 huffman 2012-03-30 set up numeral reorient simproc in Num.thy
2012-03-30 huffman 2012-03-30 replace lemmas eval_nat_numeral with a simpler reformulation
2012-03-30 huffman 2012-03-30 new lemmas for simplifying subtraction on nat numerals
2012-03-30 huffman 2012-03-30 move more theorems from Nat_Numeral.thy to Num.thy
2012-03-30 huffman 2012-03-30 fix search-and-replace errors
2012-03-30 huffman 2012-03-30 add constant pred_numeral k = numeral k - (1::nat); replace several simp rules from Nat_Numeral.thy with new ones that use pred_numeral
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-29 huffman 2012-03-29 bootstrap Num.thy before Power.thy; move lemmas about powers into Power.thy
2012-03-26 huffman 2012-03-26 fix incorrect code_modulename declarations
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)