166
click to vote
TPHOL
2005
IEEE
16 years 10 days ago
2005
IEEE
Wouldn’t it be nice to be able to conveniently use ordinary real number expressions within proof assistants? In this paper we outline how this can be done within a theorem provin...