Re: [isabelle] numbers in variable names?



> (* this doesn't work *)
> lemmas NumberNew = TestNumber [where x1="a & b"]

This works:
lemmas NumberNew = TestNumber [where ?x1.0="a & b"]


?-Vars are internally indexed. If the variable name ends in a number the
index must be given explicitly to avoid ambiguity.

Tobias





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