Re: [isabelle] setup_lifting - "no relator for the type" warning
On 01/24/2013 04:31 PM, John Wickerson wrote:
Thanks again, Ondrej.
I have one further question on this topic, which can be summarised as
"How can I make the transfer method work properly inside a
In more detail: suppose I'm working inside a context that gives me
the assumption "P f" for some fixed f. I write a lemma involving f,
and begin the proof by applying the transfer method. The transfer
method *generalises* f, and thus loses the fact that P holds for it.
Just citing from The Isabelle/Isar Reference Manual:
Goals are generalized over all free variables by default; this is
necessary for variables whose types change, but can be overridden for
specific variables with e.g. transfer fixing: x y z.
This archive was generated by a fusion of
Pipermail (Mailman edition) and