Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Variable index

Email Gateway (Aug 17 2022 at 13:26):

From: nipkow@in.tum.de
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

Last updated: Jan 04 2025 at 20:18 UTC