2010-08-27 ago renamed class/constant eq to equal; tuned some instantiations
2010-06-21 ago added bot instances; tuned
2009-03-23 ago Main is (Complex_Main) base entry point in library theories
2008-10-10 ago `code func` now just `code`
2008-07-07 ago absolute imports of HOL/*.thy theories
2008-06-26 ago established Plain theory and image
2008-03-27 ago explicit case names for rule list_induct2
2008-01-02 ago removed some legacy instantiations
2007-12-18 ago tuned proofs, document;
2007-12-17 ago removed legacy proofs
2007-12-10 ago switched import from Main to List
2007-12-06 ago R&F: added sgn lemma
2007-11-08 ago tuned presentation;
2007-11-08 ago avoid implicit use of prems;
2007-11-07 ago map and prefix
2007-11-05 ago misc lemmas about prefix, postfix, and parallel
2007-06-14 ago tuned proofs;
2007-06-05 ago tuned proofs;
2007-01-25 ago made executable
2006-11-17 ago more robust syntax for definition/abbreviation/notation;
2006-11-11 ago tuned proofs;
2006-02-16 ago new-style definitions/abbreviations;
2006-01-21 ago tuned proofs;
2005-11-25 ago tuned induct proofs;
2005-08-31 ago reactivate postfix by change of syntax;
2004-12-01 ago Removed postfix >= because of new >= sugar
2004-08-18 ago import -> imports
2004-08-16 ago New theory header syntax.
2004-06-21 ago Merged in license change from Isabelle2004
2004-05-06 ago tuned document;
2004-04-12 ago removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
2003-12-18 ago *** empty log message ***
2001-12-01 ago renamed class "term" to "type" (actually "HOL.type");
2001-10-30 ago tuned induct proofs;
2001-10-15 ago GPLed;
2001-01-11 ago added strict_prefixI', strict_prefixE';
2000-11-22 ago tuned;
2000-11-06 ago improved: 'induct' handle non-atomic goals;
2000-11-03 ago proper setup of "parallel";
2000-10-25 ago "List prefixes" library theory (replaces old Lex/Prefix);