[isabelle-dev] »real« considered harmful

[Lars Noschinski]

On 24.06.2015 16:29, Larry Paulson wrote:
> This may be the problem. I don’t remember exactly what I was trying to do, only that it was very difficult. Of course nobody uses show_types any more.
At least this was the problem for me. A notorious instance of the same
problem are the functions in HOL-Word, e.g. "ucast :: 'a word => 'b
word" and "uint :: 'a word => int". Getting at the types of things like
"uint (ucast 4)" in some big term happens often when verifying C
programs and is pretty annoying. Such things need a disambiguating
output syntax (at least as long as hovering in the output buffer doesn't
show the types, maybe even then).