Re: [isabelle] schematic variables in lemmas-command
On Thu, 21 Feb 2008, Peter Lammich wrote:
> 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]...").
Just add the "standard" attribute to the pipe-line.
It is often better to avoid such in-situ transformations of facts
altogether, which are slightly unreadable and also happen to interact
badly with local theory contexts (facts "in" a locale or class context
This archive was generated by a fusion of
Pipermail (Mailman edition) and