@CONFERENCE\{IMM2001-01917, author = "T. M. Rasmussen", title = "An Inductive Approach to Formalizing Notions of Number Theory Proofs", year = "2001", pages = "328-336", booktitle = "TPHOLs 2001: Supplemental Proceedings", volume = "", series = "Informatics Report Series", editor = "", publisher = "Division of Informatics, University of Edinburgh", organization = "", address = "", url = "http://www2.compute.dtu.dk/pubdb/pubs/1917-full.html" }