2010-03-20 ago added lemma infinite_Un
2010-02-07 ago remove redundant theorem attributes
2010-01-16 ago dropped some old primrecs and some constdefs
2009-12-17 ago add lemma INFM_conjI
2009-12-17 ago added lemmas about INFM/MOST
2009-03-23 ago Main is (Complex_Main) base entry point in library theories
2009-02-13 ago finiteness lemmas
2009-02-09 ago Imports Main in order to avoid the typerep problem
2008-07-07 ago absolute imports of HOL/*.thy theories
2008-07-01 ago rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM
2008-06-26 ago established Plain theory and image
2007-12-17 ago fixed ancestors
2007-12-10 ago switched import from Main to PreList
2007-06-14 ago tuned proofs;
2007-03-10 ago Renamed INF to INFM to avoid clash with INF operator defined in FixedPoint theory.
2007-02-01 ago new theorem int_infinite
2006-11-17 ago more robust syntax for definition/abbreviation/notation;
2006-11-08 ago moved theories Parity, GCD, Binomial to Library;
2006-11-07 ago renamed 'const_syntax' to 'notation';
2006-10-01 ago moved theory Infinite_Set to Library;