2010-06-10 haftmann 2010-06-10 qualified type "*"; qualified constants Pair, fst, snd, split
2010-06-08 haftmann 2010-06-08 qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
2010-06-02 nipkow 2010-06-02 added lemmas
2010-05-28 haftmann 2010-05-28 more coherent theory structure; tuned headings
2010-05-26 haftmann 2010-05-26 dropped legacy theorem bindings
2010-05-05 krauss 2010-05-05 repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)
2010-04-20 hoelzl 2010-04-20 Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-18 blanchet 2010-03-18 merged
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-18 haftmann 2010-03-18 lemma swap_inj_on, swap_product
2010-03-02 wenzelm 2010-03-02 proper (type_)notation;
2010-02-25 wenzelm 2010-02-25 modernized structure Split_Rule; tuned signature; more antiquotations;
2010-02-25 wenzelm 2010-02-25 more antiquotations;
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2010-01-14 haftmann 2010-01-14 tuned for products vs. tupled functions
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 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