src/HOL/Code_Numeral.thy
21 months ago haftmann 2017-10-08 one uniform type class for parity structures
21 months ago haftmann 2017-10-08 abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
21 months ago haftmann 2017-10-08 avoid fact name clashes
2017-06-24 haftmann 2017-06-24 more direct construction of integer_of_num; code equations for integer_of_char may rely on pattern matching on Char
2017-02-06 haftmann 2017-02-06 computation preprocessing rules to allow literals as input for computations
2017-01-09 haftmann 2017-01-09 slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
2016-12-17 haftmann 2016-12-17 more fine-grained type class hierarchy for div and mod
2016-10-16 haftmann 2016-10-16 eliminated irregular aliasses
2016-10-16 haftmann 2016-10-16 transfer rules for divides relation on integer and natural
2016-10-12 haftmann 2016-10-12 transfer lifting rule for numeral
2016-09-26 haftmann 2016-09-26 syntactic type class for operation mod named after mod; simplified assumptions of type class semiring_div
2016-05-29 haftmann 2016-05-29 do not export abstract constructors in code_reflect
2015-12-18 Andreas Lochbihler 2015-12-18 add serialisation for abs on integer to target language operation
2015-09-27 haftmann 2015-09-27 monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
2015-09-27 haftmann 2015-09-27 more selective preprocessing allows bare "numeral" occurences to be retained as real function in generated code
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-08-08 haftmann 2015-08-08 direct bootstrap of integer division from natural division
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-06-23 paulson 2015-06-23 Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
2015-06-01 haftmann 2015-06-01 separate class for division operator, with particular syntax added in more specific classes
2015-03-23 haftmann 2015-03-23 distributivity of partial minus establishes desired properties of dvd in semirings
2015-02-06 haftmann 2015-02-06 default abstypes and default abstract equations make technical (no_code) annotation superfluous
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-18 haftmann 2014-09-18 always annotate potentially polymorphic Haskell numerals
2014-09-18 haftmann 2014-09-18 tuned
2014-09-19 blanchet 2014-09-19 keep obsolete interpretations in Main, to avoid merge trouble
2014-09-18 blanchet 2014-09-18 reintroduced an instantiation of 'size' for 'numerals'
2014-09-18 blanchet 2014-09-18 moved old 'size' generator together with 'old_datatype'
2014-09-11 blanchet 2014-09-11 renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-05-04 blanchet 2014-05-04 renamed 'xxx_size' to 'size_xxx' for old datatype package
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-02-25 kuncar 2014-02-25 unregister lifting setup following the best practice of Lifting
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-12 Andreas Lochbihler 2014-02-12 merged
2014-02-12 Andreas Lochbihler 2014-02-12 make integer_of_char and char_of_integer work with NBE and code_simp
2014-02-12 blanchet 2014-02-12 adapted theories to 'xxx_case' to 'case_xxx' * * * 'char_case' -> 'case_char' and same for 'rec' * * * compile * * * renamed 'xxx_case' to 'case_xxx'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-08-18 haftmann 2013-08-18 execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
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-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