src/HOL/Lambda/WeakNorm.thy
2007-08-24 haftmann 2007-08-24 overloaded definitions accompanied by explicit constants
2007-08-20 haftmann 2007-08-20 renamed code_gen to export_code
2007-08-13 haftmann 2007-08-13 renamed keyword "to" to "module_name"
2007-08-10 haftmann 2007-08-10 new structure for code generator modules
2007-07-16 haftmann 2007-07-16 dropped outer ROOT structure for generated code
2007-07-11 berghofe 2007-07-11 - Renamed inductive2 to inductive - Renamed some theorems about transitive closure for predicates
2007-06-21 wenzelm 2007-06-21 tuned proofs -- avoid implicit prems;
2007-06-15 berghofe 2007-06-15 Locally added definition of "int :: nat => int" again to make code generation work.
2007-05-10 berghofe 2007-05-10 Moved extraction_expand declaration of listall_def outside of definition.
2007-05-10 haftmann 2007-05-10 consts in consts_code Isar commands are now referred to by usual term syntax
2007-05-06 haftmann 2007-05-06 changed code generator invocation syntax
2007-04-26 haftmann 2007-04-26 moved code generation pretty integers and characters to separate theories
2007-03-23 haftmann 2007-03-23 fixed typing bug in generated code
2007-03-23 haftmann 2007-03-23 fixed typing bug in generated code
2007-03-22 haftmann 2007-03-22 fixed code generator setup
2007-02-07 berghofe 2007-02-07 Adapted to new inductive definition package.
2006-11-27 haftmann 2006-11-27 removed HOL structure
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-13 haftmann 2006-11-13 adjusted name in generated code
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-11-06 haftmann 2006-11-06 (adjustions)
2006-10-31 haftmann 2006-10-31 adapted to new serializer syntax
2006-10-13 haftmann 2006-10-13 added codegen2 example
2006-10-10 haftmann 2006-10-10 purged some ML legacy
2006-10-02 haftmann 2006-10-02 cleaned mess
2006-09-26 haftmann 2006-09-26 renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
2006-09-01 haftmann 2006-09-01 final syntax for some Isar code generator keywords
2006-06-14 haftmann 2006-06-14 slight adaption for code generator
2006-06-06 haftmann 2006-06-06 added arbitray setup for codegen 2
2006-05-16 wenzelm 2006-05-16 tuned concrete syntax -- abbreviation/const_syntax;
2006-04-09 wenzelm 2006-04-09 tuned syntax/abbreviations;
2006-04-08 wenzelm 2006-04-08 refined 'abbreviation';
2006-02-16 wenzelm 2006-02-16 new-style definitions/abbreviations;
2005-12-23 wenzelm 2005-12-23 tuned proofs;
2005-12-02 berghofe 2005-12-02 Factored out proof for normalization of applications (norm_list).
2005-11-25 wenzelm 2005-11-25 tuned induct proofs;
2005-11-23 wenzelm 2005-11-23 tuned induction proofs;
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-08-25 berghofe 2005-08-25 Adapted to new code generator syntax.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-10 paulson 2005-05-10 oops...cannot use subst here
2005-05-09 paulson 2005-05-09 from simplesubst to new subst
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-02 berghofe 2005-02-02 Replaced application of subst by simplesubst in proof of app_Var_NF to avoid problems with program extraction.
2004-10-11 nipkow 2004-10-11 Proofs needed to be updated because induction now preserves name of induction variable.
2004-06-01 berghofe 2004-06-01 Adapted to new name mangling function in code generator.
2003-06-24 berghofe 2003-06-24 New proof of weak normalization with program extraction.