Now I am using Mizar to write an article on computability theory,which includes mainly general recursive functions, primitive recursive functions,and Turing's theory of computing machine etc. Did anybody do this work or have experiences with this field ? Any comments and suggestions will be appreciated. Jingchao Chen