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:

http://isabelle.in.tum.de/repos/isabelle/rev/07a8904f8fcd

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 control.


	Makarius





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