A computer assistant for a formal mathematical language : the construction of a user friendly assistant program to enter, check, store and view Weak Type Theory descriptions