src/HOL/Library/Efficient_Nat.thy
2010-08-27 ago renamed class/constant eq to equal; tuned some instantiations
2010-08-26 ago tuned includes
2010-08-26 ago code_include Scala: qualify module nmae
2010-07-26 ago corrected range check once more
2010-07-24 ago another refinement chapter in the neverending numeral story
2010-07-23 ago avoid unreliable Haskell Int type
2010-07-20 ago avoid deprecation
2010-07-19 ago dropped superfluous prefixes
2010-07-16 ago corrected range chec
2010-06-08 ago tuned quotes, antiquotations and whitespace
2010-06-01 ago corrected implementation
2010-05-21 ago nats in Haskell are readable
2010-04-30 ago renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
2010-04-16 ago replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-10 ago fixed typo
2010-03-07 ago modernized structure Object_Logic;
2010-01-22 ago code literals: distinguish numeral classes by different entries
2010-01-14 ago dedicated conversions to and from Int
2010-01-14 ago added Scala setup
2010-01-13 ago function transformer preprocessor applies to both code generators
2009-10-30 ago tuned code setup
2009-10-29 ago adjusted to changes in theory Divides
2009-09-23 ago Code_Eval(uation)
2009-07-31 ago repair mess produced by resolution afterwards
2009-07-15 ago additional preprocessor rule
2009-07-14 ago prefer code_inline over code_unfold; use code_unfold_post where appropriate
2009-07-14 ago code attributes use common underscore convention
2009-07-07 ago Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
2009-06-02 ago OCaml builtin intergers are elusive; avoid
2009-05-30 ago corrected bound/unbounded flag for nat numerals
2009-05-19 ago String.literal replaces message_string, code_numeral replaces (code_)index
2009-05-19 ago moved Code_Index, Random and Quickcheck before Main
2009-05-12 ago adapted to changes in module Code
2009-05-11 ago clarified matter of "proper" flag in code equations
2009-03-23 ago Main is (Complex_Main) base entry point in library theories
2009-02-16 ago faster preprocessor
2009-02-16 ago dropped clause_suc_preproc for generic code generator
2009-02-06 ago mandatory prefix for index conversion operations
2009-02-03 ago changed name space policy for Haskell includes
2009-01-28 ago slightly adapted towards more uniformity with div/mod on nat
2009-01-01 ago eliminated OldTerm.(add_)term_consts;
2008-12-31 ago moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-30 ago canonical Term.add_var_names;
2008-12-04 ago change more lemmas to avoid using iszero
2008-10-27 ago slightly tuned
2008-10-24 ago more clever module name aliasses for code generation
2008-10-10 ago `code func` now just `code`
2008-10-07 ago only one theorem table for both code generators
2008-09-30 ago clarified codegen interfaces
2008-09-25 ago non left-linear equations for nbe
2008-09-25 ago discontinued special treatment of op = vs. eq_class.eq
2008-09-16 ago evaluation using code generator
2008-07-21 ago fixed code generator setup
2008-07-15 ago tuned code theorem bookkeeping
2008-07-14 ago simpsets as pre/postprocessors; generic preprocessor now named function transformators
2008-07-08 ago fix: using IntInf.int for SML
2008-06-26 ago established Plain theory and image
2008-03-28 ago not depends on Main any longer
2008-02-20 ago using only an relation predicate to construct div and mod
2008-01-29 ago treating division by zero properly