[isabelle] schematic variables in lemmas-command
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.
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and