src/HOL/ex/Numeral.thy
2009-07-02 wenzelm 2009-07-02 renamed NamedThmsFun to Named_Thms; simplified/unified names of instances of Named_Thms;
2009-04-30 huffman 2009-04-30 used named theorems for declaring numeral simps
2009-04-30 huffman 2009-04-30 clean up unsigned numeral proofs
2009-04-30 huffman 2009-04-30 detect error cases in mk_num, dest_num
2009-04-29 huffman 2009-04-29 add semiring_assoc_fold simproc for unsigned numerals
2009-04-29 huffman 2009-04-29 reorient simproc for unsigned numerals
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-03-27 huffman 2009-03-27 add more lemmas for signed comparisons
2009-02-19 huffman 2009-02-19 add more ordering lemmas
2009-02-17 huffman 2009-02-17 add lemmas for exponentiation
2009-02-16 huffman 2009-02-16 tune section headings; add square function
2009-02-16 huffman 2009-02-16 merged
2009-02-16 huffman 2009-02-16 rearrange subsections
2009-02-16 huffman 2009-02-16 remove instances num::semiring and num::linorder
2009-02-16 huffman 2009-02-16 datatype num = One | Dig0 num | Dig1 num
2009-02-16 huffman 2009-02-16 replace 1::num with One; remove monoid_mult instance
2009-02-15 huffman 2009-02-15 replace dec with double-and-decrement function
2009-02-16 haftmann 2009-02-16 tuned texts
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2008-11-17 haftmann 2008-11-17 tuned unfold_locales invocation
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-09-26 haftmann 2008-09-26 op = vs. eq
2008-08-28 haftmann 2008-08-28 no parameter prefix for class interpretation
2008-08-27 haftmann 2008-08-27 added HOL/ex/Numeral.thy