src/HOL/Product_Type.thy
2007-09-25 haftmann 2007-09-25 datatype interpretators for size and datatype_realizer
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-08-07 haftmann 2007-08-07 split off theory Option for benefit of code generator
2007-06-05 haftmann 2007-06-05 merged Code_Generator.thy into HOL.thy
2007-05-09 haftmann 2007-05-09 moved recfun_codegen.ML to Code_Generator.thy
2007-05-06 haftmann 2007-05-06 tuned
2007-04-20 haftmann 2007-04-20 Isar definitions are now added explicitly to code theorem table
2007-04-04 wenzelm 2007-04-04 ML antiquotes;
2007-03-12 wenzelm 2007-03-12 syntax: proper body priorty for derived binders;
2007-03-02 haftmann 2007-03-02 using "fst" "snd" for Haskell code
2007-02-23 haftmann 2007-02-23 slight cleanup
2006-12-27 haftmann 2006-12-27 moved code generator product setup here
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-13 haftmann 2006-11-13 added thy dependencies
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-11-06 haftmann 2006-11-06 two further lemmas on split
2006-10-16 haftmann 2006-10-16 moved HOL code generator setup to Code_Generator
2006-09-19 haftmann 2006-09-19 added operational equality
2006-08-25 paulson 2006-08-25 explicit type variables prevent empty sorts
2006-08-14 haftmann 2006-08-14 simplified code generator setup
2006-07-12 haftmann 2006-07-12 adaptions in codegen
2006-07-08 wenzelm 2006-07-08 simprocs: no theory argument -- use simpset context instead;
2006-05-16 wenzelm 2006-05-16 tuned concrete syntax -- abbreviation/const_syntax;
2006-05-02 wenzelm 2006-05-02 replaced syntax/translations by abbreviation; tuned proofs; tuned;
2006-03-03 nipkow 2006-03-03 changed and retracted change of location of code lemmas.
2006-02-25 haftmann 2006-02-25 improved codegen bootstrap
2006-02-20 haftmann 2006-02-20 slight code generator serialization improvements
2006-02-14 haftmann 2006-02-14 added theory of executable rational numbers
2006-02-10 haftmann 2006-02-10 improved code generator devarification
2006-02-07 haftmann 2006-02-07 slight improvements in code generation
2006-01-23 haftmann 2006-01-23 removed problematic keyword 'atom'
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-19 berghofe 2006-01-19 Re-inserted consts_code declaration accidentally deleted during last commit.
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2005-12-29 haftmann 2005-12-29 adaptions to changes in code generator
2005-12-08 wenzelm 2005-12-08 tuned proofs;
2005-12-02 haftmann 2005-12-02 adjusted to improved code generator interface
2005-12-01 wenzelm 2005-12-01 simprocs: static evaluation of simpset;
2005-11-22 haftmann 2005-11-22 added codegenerator
2005-10-28 haftmann 2005-10-28 added extraction interface for code generator
2005-10-21 wenzelm 2005-10-21 Goal.prove;
2005-10-17 wenzelm 2005-10-17 change_claset/simpset; Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-10-07 wenzelm 2005-10-07 replaced _K by dummy abstraction;
2005-08-16 paulson 2005-08-16 more simprules now have names
2005-08-03 berghofe 2005-08-03 Fixed bug in code generator for let and split leading to ill-formed code.
2005-08-02 wenzelm 2005-08-02 simprocs: Simplifier.inherit_bounds;
2005-07-12 berghofe 2005-07-12 Auxiliary functions to be used in generated code are now defined using "attach".
2005-07-01 berghofe 2005-07-01 Adapted to new interface of code generator.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-31 wenzelm 2005-05-31 tuned;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-12-18 schirmer 2004-12-18 added print translation for split: split f --> %(x,y). f x y
2004-12-13 paulson 2004-12-13 removal of NatArith.ML and Product_Type.ML
2004-12-10 berghofe 2004-12-10 New code generator for let and split.
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-06-16 paulson 2004-06-16 removal of x-symbol syntax <Sigma> for dependent products