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 
etc.).


	Makarius





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