src/HOL/ex/Numeral.thy
2011-10-16 haftmann 2011-10-16 tuned proof
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-04-06 wenzelm 2011-04-06 discontinued old-style Syntax.constrainC;
2011-04-06 wenzelm 2011-04-06 typed_print_translation: discontinued show_sorts argument;
2011-04-06 wenzelm 2011-04-06 moved unparse material to syntax_phases.ML;
2011-01-10 wenzelm 2011-01-10 standardized split_last/last_elem towards List.last; eliminated obsolete Library.last_elem;
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-09-10 haftmann 2010-09-10 Haskell == is infix, not infixl
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-08-31 haftmann 2010-08-31 more coherent naming of syntax data structures
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-27 wenzelm 2010-08-27 merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
2010-08-26 haftmann 2010-08-26 prevent line breaks after Scala symbolic operators
2010-08-26 wenzelm 2010-08-26 more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
2010-07-28 haftmann 2010-07-28 tuned; added pretty numerals for code generation
2010-07-14 haftmann 2010-07-14 avoid export_code ... file -
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-03 wenzelm 2010-03-03 adapted to authentic syntax -- actual types are verbatim;
2010-02-25 wenzelm 2010-02-25 explicit @{type_syntax} markup;
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax};
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-11-08 wenzelm 2009-11-08 modernized structure Reorient_Proc; explicit merge of constituent functions, avoids exponential blowup when traversing the import graph; adapted Theory_Data; tuned;
2009-10-29 wenzelm 2009-10-29 recovered from 7a1f597f454e, simplified imports;
2009-10-29 haftmann 2009-10-29 adjusted import to changed HOL theory graph
2009-07-14 haftmann 2009-07-14 prefer code_inline over code_unfold; use code_unfold_post where appropriate
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
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