[isabelle] Reasoning behind appearance of variables in isar cases?
I am confused as to why Isabelle displays different variables than their
actual names in some cases. For instance:
lemma "P (xs::'a list)"
proof (induct xs)
thus ?case sorry
case (Cons x xs)
hence "P xs" .
Note how I write "Cons x xs" and "P xs" but Isabelle keeps displaying
xsa. With complicated induction proofs this makes it hard to keep track
of what exactly the variables are called. It doesn't prevent shadowing
because when I write "xs" I don't get the blue xs from the original
Also, when copying a subgoal or parts thereof to a new "have" or "lemma"
statement to prove them separately, I have to go through and convert
every "<var>a" to "<var>". This is cumbersome.
Why does this happen, and is there a way to turn this behaviour off?
This archive was generated by a fusion of
Pipermail (Mailman edition) and