[isabelle] Coercions rename bound variables

Hi all.

Consider the following:

imports Complex_Main

term "∃a::nat. ∃b::nat. ∃c::real. a+b+c=0"

The output is: 
"∃x xa c. real x + real xa + c = 0"
  :: "bool"

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 MHonArc.