[isabelle] Coercions rename bound variables
Consider the following:
term "∃a::nat. ∃b::nat. ∃c::real. a+b+c=0"
The output is:
"∃x xa c. real x + real xa + c = 0"
Thus, instead of my original variable names, I get synthetic names
x,xa, ..., which makes the term less readable.
Is there any special reason why the variables have to be renamed?
Otherwise, it would be nice to keep the original names.
This archive was generated by a fusion of
Pipermail (Mailman edition) and