2012-04-03 griff 2012-04-03 renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
2012-01-14 wenzelm 2012-01-14 renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
2011-12-02 wenzelm 2011-12-02 more antiquotations;
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-12-12 krauss 2010-12-12 tuned headers
2010-10-05 krauss 2010-10-05 discontinued continuations to simplify control flow; dropped optimization in scnp
2010-10-05 krauss 2010-10-05 use Cache structure instead of passing tables around explicitly
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-19 haftmann 2010-08-19 more antiquotations
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-10 haftmann 2010-06-10 tuned quotes, antiquotations and whitespace
2010-06-08 haftmann 2010-06-08 qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2010-02-27 wenzelm 2010-02-27 just one copy of structure Term_Graph (in Pure);
2010-02-27 wenzelm 2010-02-27 clarified @{const_name} vs. @{const_abbrev};
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2010-01-03 wenzelm 2010-01-03 made SML/NJ happy;
2010-01-02 krauss 2010-01-02 new year's resolution: reindented code in function package
2010-01-02 krauss 2010-01-02 simplified
2010-01-02 krauss 2010-01-02 absorb structures Decompose and Descent into Termination, to simplify further restructuring
2009-11-23 krauss 2009-11-23 eliminated dead code and some unused bindings, reported by polyml
2009-10-23 krauss 2009-10-23 function package: more standard names for structures and files
2009-09-19 haftmann 2009-09-19 inter and union are mere abbreviations for inf and sup
2009-09-18 haftmann 2009-09-18 more antiquotations
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-22 haftmann 2009-07-22 set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
2009-07-09 wenzelm 2009-07-09 renamed functor TableFun to Table, and GraphFun to Graph;
2009-06-23 haftmann 2009-06-23 uniformly capitialized names for subdirectories