2012-03-25 ago merged fork with new numeral representation (see NEWS)
2012-02-25 ago removing unnecessary assumptions in RealDef;
2012-01-06 ago prefer concat over foldl append []
2011-12-02 ago more antiquotations;
2011-09-12 ago new fastforce replacing fastsimp - less confusing name
2011-08-10 ago old term operations are legacy;
2011-08-02 ago moved recdef package to HOL/Library/Old_Recdef.thy
2011-03-03 ago tuned proofs -- eliminated prems;
2011-03-03 ago removed spurious 'unused_thms' (cf. 1a65b780bd56);
2011-02-25 ago Some cleaning up
2011-02-24 ago recdef -> fun(ction)
2011-02-24 ago eliminated clones of List.upto
2011-02-21 ago tuned proofs -- eliminated prems;
2011-01-07 ago adopting proofs due to new list comprehension to set comprehension simproc
2010-12-29 ago explicit file specifications -- avoid secondary load path;
2010-08-27 ago formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 ago formerly unnamed infix impliciation now named HOL.implies
2010-08-19 ago tuned quotes
2010-08-19 ago use antiquotations for remaining unqualified constants in HOL
2010-07-19 ago diff_minus subsumes diff_def
2010-05-12 ago tuned test problems
2010-05-09 ago avoid using real-specific versions of generic lemmas
2010-04-29 ago code_reflect: specify module name directly after keyword
2010-04-28 ago use code_reflect
2010-03-01 ago replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-05 ago more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-11-12 ago New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
2009-10-22 ago map_range (and map_index) combinator
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2009-07-07 ago renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
2009-06-20 ago added lemmas; tuned
2009-06-17 ago new GCD library, courtesy of Jeremy Avigad
2009-03-22 ago 1. New cancellation simprocs for common factors in inequations
2009-03-11 ago Updated paths in Decision_Procs comments and NEWS
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-02-26 ago add type annotation
2009-02-25 ago generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
2009-02-21 ago Removed subsumed lemmas
2009-02-06 ago session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there