src/HOL/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)