[isabelle] schematic variables in lemmas-command



Hi all,

I have a lemma valid_unconc, that has a variable c of list type.
Now I want to get a specialized version where c is a singleton list.
I tried
  lemmas valid_uncons = valid_unconc[where c="[s]", simplified]
but this will give a lemma where s is fixed, rather then a schematic variable ("...[s]..." instead of "...[?s]...").

The following seems to work, but I don't understand why or what else it would do if there occurred pair types in my lemma:
lemmas valid_uncons =
  valid_unconc[where c="[s]", simplified, split_format]

So is this the way to go, or is there another way to specialize a lemma as I want to do?

Thanks in advance for any hints,
  Peter






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