src/HOL/Library/Efficient_Nat.thy
2011-12-09 bulwahn 2011-12-09 deactivating quickcheck_narrowing if Efficient_Nat theory is loaded
2011-10-19 bulwahn 2011-10-19 removing old code generator setup for efficient natural numbers; cleaned typo
2011-07-02 haftmann 2011-07-02 tuned typo
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2010-11-18 haftmann 2010-11-18 map_pair replaces prod_fun
2010-09-29 haftmann 2010-09-29 scala is reserved identifier
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-10 haftmann 2010-09-10 Haskell == is infix, not infixl
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-09-01 haftmann 2010-09-01 do not print object frame around Scala includes -- this is in the responsibility of the user
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-26 haftmann 2010-08-26 tuned includes
2010-08-26 haftmann 2010-08-26 code_include Scala: qualify module nmae
2010-07-26 haftmann 2010-07-26 corrected range check once more
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-07-20 haftmann 2010-07-20 avoid deprecation
2010-07-19 haftmann 2010-07-19 dropped superfluous prefixes
2010-07-16 haftmann 2010-07-16 corrected range chec
2010-06-08 haftmann 2010-06-08 tuned quotes, antiquotations and whitespace
2010-06-01 haftmann 2010-06-01 corrected implementation
2010-05-21 haftmann 2010-05-21 nats in Haskell are readable
2010-04-30 wenzelm 2010-04-30 renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
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-10 haftmann 2010-03-10 fixed typo
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