Re: [isabelle] Writing a specific rule_tac application on ML level
On Sun, 24 Oct 2010, Alexander Krauss wrote:
Look at term_lift_inst_rule in tactic.ML, I've previously used it for (I
think) something like what you're trying to do
that function no longer exists:
The question about term-based res_inst_tac is very old (maybe 15 years).
Various people had come up with private solutions to that. More recently,
with the almost accidental advent of FOCUS, it became suddenly clear that
the answer is there.
So only thing you can't do with FOCUS is instantiate schematic variables
in the goal, but these are very rare in (robust) proofs under ML program
This archive was generated by a fusion of
Pipermail (Mailman edition) and