src/HOL/Finite.thy
2000-06-20 paulson 2000-06-20 now setsum f A = 0 unless A is finite
2000-05-24 paulson 2000-05-24 setsum is now overloaded on plus_ac0
1999-10-27 oheimb 1999-10-27 added various little lemmas
1998-12-04 paulson 1998-12-04 locales: assumes and defines may be empty
1998-10-31 paulson 1998-10-31 locales now implicitly quantify over free variables
1998-10-09 nipkow 1998-10-09 New inductive definition of `card'
1998-10-06 nipkow 1998-10-06 Merges FoldSet into Finite
1998-06-30 berghofe 1998-06-30 Adapted to new inductive package.
1997-06-05 nipkow 1997-06-05 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. Relation.ML Trancl.ML: more thms WF.ML WF.thy: added `acyclic' WF_Rel.ML: moved some thms back into WF and added some new ones.
1997-06-03 paulson 1997-06-03 New theorem about the cardinality of the powerset (uses exponentiation)
1997-05-30 paulson 1997-05-30 Now Divides must be the parent
1996-03-06 clasohm 1996-03-06 added constdefs section
1996-03-04 nipkow 1996-03-04 Added a constant UNIV == {x.True} Added many new rewrite rules for sets. Moved LEAST into Nat. Added cardinality to Finite.
1996-02-05 clasohm 1996-02-05 expanded tabs; renamed subtype to typedef; incorporated Konrad's changes
1995-11-29 clasohm 1995-11-29 removed quotes from types in consts and syntax sections
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application