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*.

Wed Mar 20 13:05:14 MET 1996