[isabelle-dev] real v of_nat

[Lawrence Paulson]

Tomorrow, I hope to start the long-proposed unification of the functions real and of_nat. The plan is to make of these two functions (along with real_of_nat) synonymous. At the moment, real and of_nat are extensionally equal but distinct functions, while real_of_nat is an abbreviation for of_nat. Afterwards, I hope to be able to eliminate real_of_nat and make real an abbreviation for of_nat.

The function “real” is overloaded for a couple of other types, including int, which is apparently seldom used, but other overloadings also exist, and some instances of the function are not even injective. These I expect to replace by functions with names like real_of_XX. This is just advanced warning, in case somebody else is working on changes involving type real.

Larry