[isabelle] Instantiate schematic variable in apply-script



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)

Best,
  Peter






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