[isabelle] Coercions rename bound variables



Hi all.

Consider the following:

imports Complex_Main
begin

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.

--
  Peter





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.