src/HOL/Product_Type.thy
2010-01-13 haftmann 2010-01-13 some syntax setup for Scala
2009-11-25 haftmann 2009-11-25 bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
2009-11-12 hoelzl 2009-11-12 Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute
2009-11-10 haftmann 2009-11-10 lemmas about apfst and apsnd
2009-10-28 haftmann 2009-10-28 load Product_Type before Nat; dropped junk
2009-10-28 paulson 2009-10-28 New theory Probability, which contains a development of measure theory
2009-10-24 wenzelm 2009-10-24 import theory Nat here, which avoids duplicate definition of datatype_realizers (and thus allows to maintain fully authentic fact table);
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-06-23 haftmann 2009-06-23 uniformly capitialized names for subdirectories
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-16 haftmann 2009-06-16 dropped ID
2009-06-10 haftmann 2009-06-10 separate directory for datatype package
2009-05-19 haftmann 2009-05-19 pretty printing of functional combinators for evaluation code
2009-04-15 haftmann 2009-04-15 default instantiation for unit type
2009-03-20 berghofe 2009-03-20 split_codegen now eta-expands terms on-the-fly.
2008-11-06 nipkow 2008-11-06 added lemma
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-10-09 haftmann 2008-10-09 established canonical argument order in SML code generators
2008-09-25 haftmann 2008-09-25 discontinued special treatment of op = vs. eq_class.eq
2008-09-17 wenzelm 2008-09-17 back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-06-10 haftmann 2008-06-10 rep_datatype command now takes list of constructors as input arguments
2008-05-23 berghofe 2008-05-23 Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that set print_mode and margin appropriately.
2008-05-07 berghofe 2008-05-07 split_beta is now declared as monotonicity rule, to allow bounded quantifiers in introduction rules of inductive predicates.
2008-04-09 haftmann 2008-04-09 removed syntax from monad combinators; renamed mbind to scomp
2008-03-29 wenzelm 2008-03-29 replaced 'ML_setup' by 'ML';
2008-03-20 haftmann 2008-03-20 Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
2008-03-19 wenzelm 2008-03-19 more antiquotations; eliminated change_claset/simpset;
2008-02-26 bulwahn 2008-02-26 Added useful general lemmas from the work with the HeapMonad
2008-01-10 berghofe 2008-01-10 New interface for test data generators.
2007-12-05 haftmann 2007-12-05 simplified infrastructure for code generator operational equality
2007-11-30 haftmann 2007-11-30 more canonical attribute application
2007-10-04 haftmann 2007-10-04 certificates for code generator case expressions
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