presented at event 18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2011)/10th International Conference on Mathematical Knowledge Management (MKM 2011) Conference