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-09-01 wenzelm 2010-09-01 eliminated really ancient OldGoals operations in favour of Goal.prove_internal (with its minimal checks and without normalization of result); tuned white space; tuned indentation;
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-06-01 berghofe 2010-06-01 merged
2010-06-01 berghofe 2010-06-01 Adapted to new format of proof terms containing explicit proofs of class membership.
2010-05-26 haftmann 2010-05-26 dropped legacy theorem bindings
2010-05-08 wenzelm 2010-05-08 renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
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-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;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-25 wenzelm 2010-02-25 more antiquotations;
2009-11-30 haftmann 2009-11-30 dropped some unused bindings
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-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
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-09-28 haftmann 2009-09-28 avoid compound fields in datatype info record
2009-09-27 haftmann 2009-09-27 registering split rules and projected induction rules; ML identifiers more close to Isar theorem names
2009-07-16 wenzelm 2009-07-16 eliminated legacy_varify;
2009-06-23 haftmann 2009-06-23 tuned interfaces of datatype module
2009-06-23 haftmann 2009-06-23 uniformly capitialized names for subdirectories