In my tactic implementation, I would like to call
resolve_tac on a fixed theorem, called
mytheorem. However, I would like to first instantiate a schematic variable based on my previous computation. In vanilla Isabelle, I would have written
mytheorem[of t]. How do I do it in ML when
t is stored in a ML variable?
Have you tried
For discovery purpose: I did not remember, so I grepped 'instantiate' on
~~src/HOL/Tools/SMT (but I am biased, because I have written some of the code there). If that had failed, I would have search for the type I expect on
ok thx for the trick.
Last updated: Dec 07 2023 at 12:30 UTC