[isabelle] Variable index



PS If you use "\<^isub>" to index your names at the end, it looks nicer and
your command would have worked:

lemma TestNumber: "x\<^isub>1 --> x\<^isub>1"
by (simp)

lemmas NumberNew = TestNumber [where x\<^isub>1="a & b"]

Tobias





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