2011-04-19 wenzelm 2011-04-19 eliminated Codegen.mode in favour of explicit argument;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-12-31 wenzelm 2010-12-31 do not open structure Codegen;
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-12-01 wenzelm 2010-12-01 more direct use of binder_types/body_type;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-18 haftmann 2010-08-18 liberal instantiation of class eq; tuned naming scheme
2010-08-11 haftmann 2010-08-11 moved instantiation target formally to class_target.ML
2010-06-14 haftmann 2010-06-14 explicitly name and note equations for class eq
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-22 haftmann 2010-04-22 swapped generic code generator and SML code generator
2010-03-22 wenzelm 2010-03-22 explicit Simplifier.global_context;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2009-11-30 haftmann 2009-11-30 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-11-27 haftmann 2009-11-27 renamed former datatype.ML to datatype_data.ML
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-10 wenzelm 2009-11-10 modernized structure Theory_Target;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-10-20 wenzelm 2009-10-20 merged
2009-10-20 haftmann 2009-10-20 more accurate checkpoints
2009-10-19 haftmann 2009-10-19 dropped lazy code equations
2009-10-19 wenzelm 2009-10-19 uniform use of Integer.add/mult/sum/prod;
2009-10-17 wenzelm 2009-10-17 operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
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-10-12 haftmann 2009-10-12 using distinct rules directly
2009-10-08 haftmann 2009-10-08 lookup for datatype constructors considers type annotations to resolve overloading
2009-06-23 haftmann 2009-06-23 tuned interfaces of datatype module
2009-06-23 haftmann 2009-06-23 uniformly capitialized names for subdirectories