[isabelle] numbers in variable names?



Is it possible to use numbers in variable names? I thought it was, but then ran into a problem shown in the theory below. It seems like it should work, unless I don't understand something...

theory Scratch = Main:

a TestLetter: "x --> x"
by (simp)

lemma TestNumber: "x1 --> x1"
by (simp)

lemmas LetterNew = TestLetter [where x="a & b"]
thm LetterNew

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

end






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