Text this: Interfacing external CA systems for Grobner bases computation in Mizar proof checking.