On 03.07.2015 04:02, Daniel Matichuk wrote:
> Additionally, fresh names are chosen for any free variables that appear in
> the subgoal
>
> e.g.
>
> lemma "⋀x y. A x y"
> subgoal for A
>
> Results in "x" being named "Aa". In this case I would expect either an error
> ("Free name clash") or for the new fixed term to shadow the free A.
> The second choice is a bit strange, however, because you end up with two
> different coloured "A"s in the goal.
I would expect unspecified variables to get internal names, i.e. names
ending with "_"; similar to variables not specified in a case command.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
