------------------------------------------------------------------------
Top of finite sets theory Version 2.2 5/22/97
--------------------------------------------------------------
Authors: Ricky W. Butler NASA Langley Research Center
Bruno Dutertre Royal Holloway & Bedford New College
Damir Jamsek Odyssey Research Associates
Sam Owre SRI International
David Griffioen CWI and KUN (Catholic University
Nijmegen), the Netherlands.
Index:
------
finite sets -- main theory that is imported
(provides basic type and cardinality)
finite sets sum -- summation over a set
finite sets minmax -- min and max over a set
finite sets inductions -- induction schemes
finite sets sum real -- additional properties for summations
over real-valued functions
finite sets int -- special properties of integer sets
finite sets nat -- special properties of natural sets
finite sets pred -- lemmas involving predicate subtypes
finite sets below -- lemmas involving sets of below and upto
finite sets eq -- lemmas to show set is finite via mappings
finite sets card eq -- equal cardinality of two dissimilar sets
finite_sets_rules -- experimental AUTO-REWRITE-THEORY rules
This theory was designed for making libraries and is not intended
for importing. One should directly import one of the above listed
theories.
------------------------------------------------------------------------