# [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.*