src/HOL/Code_Numeral.thy
2013-03-08 kuncar 2013-03-08 patch Isabelle ditribution to conform to changes regarding the parametricity
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
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-07-23 haftmann 2012-07-23 restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
2012-04-01 huffman 2012-04-01 removed Nat_Numeral.thy, moving all theorems elsewhere
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-02-24 haftmann 2012-02-24 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24 haftmann 2012-02-24 given up disfruitful branch
2012-02-23 haftmann 2012-02-23 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-20 huffman 2012-02-20 use qualified constant names instead of suffixes (from Florian Haftmann)
2011-12-29 haftmann 2011-12-29 attribute code_abbrev superseedes code_unfold_post
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-09-07 huffman 2011-09-07 avoid using legacy theorem names
2010-10-01 haftmann 2010-10-01 use module integer for Eval
2010-09-10 haftmann 2010-09-10 Haskell == is infix, not infixl
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-07-24 haftmann 2010-07-24 another refinement chapter in the neverending numeral story
2010-07-23 haftmann 2010-07-23 avoid unreliable Haskell Int type
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-31 bulwahn 2010-03-31 adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
2010-03-10 haftmann 2010-03-10 tuned whitespace
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-22 haftmann 2010-01-22 code literals: distinguish numeral classes by different entries
2010-01-15 berghofe 2010-01-15 merged
2010-01-10 berghofe 2010-01-10 Adapted to changes in induct method.
2010-01-14 haftmann 2010-01-14 allow individual printing of numerals during code serialization
2010-01-13 haftmann 2010-01-13 some syntax setup for Scala
2009-10-29 haftmann 2009-10-29 moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-10-29 haftmann 2009-10-29 moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-10-28 haftmann 2009-10-28 moved theory Divides after theory Nat_Numeral; tuned some proof texts
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-06-02 haftmann 2009-06-02 OCaml builtin intergers are elusive; avoid
2009-05-27 haftmann 2009-05-27 added lemma about 0 - 1
2009-05-19 haftmann 2009-05-19 String.literal replaces message_string, code_numeral replaces (code_)index