src/HOL/Finite_Set.thy
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2004-04-01 paulson 2004-04-01 new type class abelian_group
2004-03-25 paulson 2004-03-25 new material from Avigad
2004-03-10 paulson 2004-03-10 strengthened the axclass claims
2004-03-08 paulson 2004-03-08 generic theorems about exponentials; general tidying up
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2003-12-27 paulson 2003-12-27 re-organized numeric lemmas
2003-12-19 nipkow 2003-12-19 *** empty log message ***
2003-09-26 paulson 2003-09-26 misc tidying
2003-02-20 paulson 2003-02-20 new inverse image lemmas
2002-11-29 nipkow 2002-11-29 added a few lemmas
2002-11-28 ballarin 2002-11-28 HOL-Algebra partially ported to Isar.
2002-11-13 berghofe 2002-11-13 Transitive closure is now defined inductively as well.
2002-09-27 paulson 2002-09-27 Proof tidying
2002-09-20 paulson 2002-09-20 less use of x-symbols
2002-08-12 nipkow 2002-08-12 Added Mi and Max on sets, hid Min and Pls on numerals.
2002-07-24 wenzelm 2002-07-24 simplified locale predicates;
2002-07-19 wenzelm 2002-07-19 accomodate cumulative locale predicates;
2002-07-18 wenzelm 2002-07-18 ACe_axioms;
2002-07-16 wenzelm 2002-07-16 adapted to locale defs;
2002-02-25 wenzelm 2002-02-25 clarified syntax of ``long'' statements: fixes/assumes/shows;
2002-01-11 wenzelm 2002-01-11 lemmas (in ACe) AC;
2002-01-10 wenzelm 2002-01-10 qualified exports from locales;
2001-12-06 wenzelm 2001-12-06 renamed theory Finite to Finite_Set and converted;