src/HOL/Library/EfficientNat.thy
2007-06-14 wenzelm 2007-06-14 tuned proofs;
2007-06-13 huffman 2007-06-13 removed constant int :: nat => int; int is now an abbreviation for of_nat :: nat => int
2007-06-05 wenzelm 2007-06-05 simplified/renamed add_numerals;
2007-05-19 haftmann 2007-05-19 uniform module names for code generation
2007-05-10 haftmann 2007-05-10 beta/eta conversion after preprocessor
2007-05-10 haftmann 2007-05-10 consts in consts_code Isar commands are now referred to by usual term syntax
2007-05-10 wenzelm 2007-05-10 moved conversions to structure Conv;
2007-05-06 haftmann 2007-05-06 changed code generator invocation syntax
2007-04-26 haftmann 2007-04-26 tuned
2007-04-20 haftmann 2007-04-20 improved case unfolding
2007-03-23 haftmann 2007-03-23 tuned
2007-03-09 haftmann 2007-03-09 dropped code datatype certificates
2007-03-02 haftmann 2007-03-02 improved handling of nat numerals
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-02-14 haftmann 2007-02-14 clarified explanation
2007-01-09 haftmann 2007-01-09 named preprocessors
2006-12-27 haftmann 2006-12-27 added OCaml code generation (without dictionaries)
2006-12-18 haftmann 2006-12-18 dropped two inline directives
2006-12-14 wenzelm 2006-12-14 proper use of IntInf instead of InfInf;
2006-12-13 haftmann 2006-12-13 introduced mk/dest_numeral/number for mk/dest_binum etc.
2006-11-27 haftmann 2006-11-27 removed HOL structure
2006-11-22 haftmann 2006-11-22 dropped eq const
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-10 wenzelm 2006-11-10 tuned Variable.trade;
2006-11-06 haftmann 2006-11-06 code generator module naming improved
2006-10-31 haftmann 2006-10-31 adapted to new serializer syntax
2006-10-31 haftmann 2006-10-31 adapted to new serializer syntax
2006-10-16 haftmann 2006-10-16 moved HOL code generator setup to Code_Generator
2006-10-10 haftmann 2006-10-10 gen_rem(s) abandoned in favour of remove / subtract
2006-10-02 haftmann 2006-10-02 improvements for code_gen
2006-09-26 haftmann 2006-09-26 renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
2006-09-25 haftmann 2006-09-25 updated theory description
2006-09-20 haftmann 2006-09-20 improvements for codegen 2
2006-09-19 haftmann 2006-09-19 code generation 2 adjustments
2006-09-13 krauss 2006-09-13 Major update to function package, including new syntax and the (only theoretical) ability to handle local contexts.
2006-09-01 haftmann 2006-09-01 final syntax for some Isar code generator keywords
2006-08-08 haftmann 2006-08-08 improvements for 2nd codegenerator
2006-08-02 wenzelm 2006-08-02 replaced obsolete standard/freeze_all by Variable.trade;
2006-07-25 wenzelm 2006-07-25 renamed add_term_varnames to Term.add_varnames (cf. Term.add_vars etc.);
2006-07-12 haftmann 2006-07-12 adaptions in codegen
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-06-14 haftmann 2006-06-14 slight adaptions for code generator
2006-06-08 berghofe 2006-06-08 Removed "code del" declarations again.
2006-06-06 haftmann 2006-06-06 refined code generation
2006-05-11 wenzelm 2006-05-11 avoid raw equality on type thm;
2006-05-09 haftmann 2006-05-09 added preprocs for CodegenTheorems
2006-04-27 paulson 2006-04-27 renamed HOLogic.mk_bin to mk_binum for consistency with dest_binum
2006-02-25 haftmann 2006-02-25 change in codegen syntax
2006-02-15 haftmann 2006-02-15 some fixes
2006-01-30 haftmann 2006-01-30 adaptions to codegen_package
2006-01-23 haftmann 2006-01-23 removed problematic keyword 'atom'
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2005-07-22 berghofe 2005-07-22 Rewrote function remove_suc, since it failed on some equations produced by recdef.
2005-07-15 wenzelm 2005-07-15 tuned fold on terms;
2005-07-12 berghofe 2005-07-12 Auxiliary functions to be used in generated code are now defined using "attach".
2005-06-06 berghofe 2005-06-06 Added code lemma for <
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.