[Logiweb] Naming variables in proofs

[Klaus Ebbe Grue]

Hi logiweb at diku.dk

On Sat, 4 Jun 2005, Frederik Eriksen wrote:
>
> It seems to me that sometimes it makes a difference how you name the 
> variables of your proof...

The problem is traced down now. I publish a new base page later to solve 
the problem (later means: when I return Wednesday next week or later).

Until then, beware of strange behaviour of "var x", "meta x", and 
"peano x".

Klaus

PS The problem is that the index of the base page contains an entry that 
defines the "tactic" aspect of "var x" to be "var y", which is nonsense. 
I forgot to disable that definition, so Logiweb thinks the variable "var 
x" actually is a proof tactic to be expanded a proof check time. "var x" 
is also defined in many other peculiar ways in the index. "meta x" and 
"peano x" macro expand to "var x" with a "meta" or "peano" mark on it, so 
they are also affected.