Re: [isabelle] Instantiate schematic variable in apply-script



On 26.09.2011 19:02, Peter Lammich wrote:
Hi all,

I have a subgoal of the form
[| ... |] ==>  a = ?f x

The proof is to instantiate ?f to function "foo", and then
invoke the simplifier. How to do this instantiation, i.e. is there a
method instantiate with that I can do:
   apply (instantiate ?f = foo)

My usual approach would be to avoid introducing ?f, i.e. sufficiently instantiate the rule which introduced ?f (using the [of]-attribute).





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