*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Coercions rename bound variables*From*: Peter Lammich <lammich at in.tum.de>*Date*: Tue, 26 Nov 2013 13:39:47 +0100

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

**Follow-Ups**:**Re: [isabelle] Coercions rename bound variables***From:*Dmitriy Traytel

- Previous by Date: Re: [isabelle] Misleading tooltips on Isabelle-Terms with coercions in isabelle/jedit
- Next by Date: Re: [isabelle] Coercions rename bound variables
- Previous by Thread: Re: [isabelle] Misleading tooltips on Isabelle-Terms with coercions in isabelle/jedit
- Next by Thread: Re: [isabelle] Coercions rename bound variables
- Cl-isabelle-users November 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list