The Contributions Library

This library is not based on the Micro Library, because it grew up independently of it. The different contributions build on one another. These contributions include the monomorphic set theory as presented in [] with all the elimination constants and also their reading as logical constants; arithmetic with natural numbers; some results about the algebraic structure of integers and some basic functions and properties on lists. The library is organized as follows:

The directory M onomorphic.Set.Theory contains the following theories: E mpty, N 1, B ool, N at, S igma, P roduct, P i, F unction, U nion, I d, I d_properties.

The directory P redicate.Logic contains the theories: A bsurdity, T rue, A nd, O r, I mply, E xists, F orall.

The directory N atural.Numbers contains the theories: N at_properties, L ift, l t, p lus, m ult, d iv, m onus.

The directory I ntegers contains the theories: Z , p lussubs, I dZ, z sprops, z add, z addinv, z minus.

The directory L ists contains the theories l ists, l ist_props, p erms, g ensym.