src/HOL/Library/Efficient_Nat.thy
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-01-22 haftmann 2010-01-22 code literals: distinguish numeral classes by different entries
2010-01-14 haftmann 2010-01-14 dedicated conversions to and from Int
2010-01-14 haftmann 2010-01-14 added Scala setup
2010-01-13 haftmann 2010-01-13 function transformer preprocessor applies to both code generators
2009-10-30 haftmann 2009-10-30 tuned code setup
2009-10-29 haftmann 2009-10-29 adjusted to changes in theory Divides
2009-09-23 haftmann 2009-09-23 Code_Eval(uation)
2009-07-31 haftmann 2009-07-31 repair mess produced by resolution afterwards
2009-07-15 haftmann 2009-07-15 additional preprocessor rule
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-07 haftmann 2009-07-07 Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
2009-06-02 haftmann 2009-06-02 OCaml builtin intergers are elusive; avoid
2009-05-30 haftmann 2009-05-30 corrected bound/unbounded flag for nat numerals
2009-05-19 haftmann 2009-05-19 String.literal replaces message_string, code_numeral replaces (code_)index
2009-05-19 haftmann 2009-05-19 moved Code_Index, Random and Quickcheck before Main
2009-05-12 haftmann 2009-05-12 adapted to changes in module Code
2009-05-11 haftmann 2009-05-11 clarified matter of "proper" flag in code equations
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2009-02-16 haftmann 2009-02-16 faster preprocessor
2009-02-16 haftmann 2009-02-16 dropped clause_suc_preproc for generic code generator
2009-02-06 haftmann 2009-02-06 mandatory prefix for index conversion operations
2009-02-03 haftmann 2009-02-03 changed name space policy for Haskell includes
2009-01-28 haftmann 2009-01-28 slightly adapted towards more uniformity with div/mod on nat
2009-01-01 wenzelm 2009-01-01 eliminated OldTerm.(add_)term_consts;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-30 wenzelm 2008-12-30 canonical Term.add_var_names;
2008-12-04 huffman 2008-12-04 change more lemmas to avoid using iszero
2008-10-27 haftmann 2008-10-27 slightly tuned
2008-10-24 haftmann 2008-10-24 more clever module name aliasses for code generation
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-10-07 haftmann 2008-10-07 only one theorem table for both code generators
2008-09-30 haftmann 2008-09-30 clarified codegen interfaces
2008-09-25 haftmann 2008-09-25 non left-linear equations for nbe
2008-09-25 haftmann 2008-09-25 discontinued special treatment of op = vs. eq_class.eq
2008-09-16 haftmann 2008-09-16 evaluation using code generator
2008-07-21 haftmann 2008-07-21 fixed code generator setup
2008-07-15 haftmann 2008-07-15 tuned code theorem bookkeeping
2008-07-14 haftmann 2008-07-14 simpsets as pre/postprocessors; generic preprocessor now named function transformators
2008-07-08 haftmann 2008-07-08 fix: using IntInf.int for SML
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-03-28 haftmann 2008-03-28 not depends on Main any longer
2008-02-20 haftmann 2008-02-20 using only an relation predicate to construct div and mod
2008-01-29 haftmann 2008-01-29 treating division by zero properly
2008-01-25 haftmann 2008-01-25 fixed and tuned
2008-01-21 haftmann 2008-01-21 streamlined and improved
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2008-01-10 berghofe 2008-01-10 New interface for test data generators.
2008-01-02 haftmann 2008-01-02 index now a copy of nat rather than int
2007-12-13 haftmann 2007-12-13 target language div and mod
2007-11-28 haftmann 2007-11-28 deleted looping code theorem
2007-10-12 haftmann 2007-10-12 consolidated naming conventions for code generator theories
2007-09-25 haftmann 2007-09-25 Efficient_Nat and Pretty_Int integrated with ML_Int
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated IntInf.int, integer);
2007-08-24 haftmann 2007-08-24 overloaded definitions accompanied by explicit constants
2007-08-10 haftmann 2007-08-10 new structure for code generator modules
2007-08-09 haftmann 2007-08-09 tuned
2007-07-19 haftmann 2007-07-19 uniform naming conventions for CG theories