Theorem Proving with the Real Numbers door John Harrison