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)