Re: [isabelle] Creating simple tactics
On Sat, 24 Dec 2005, Greg Bronevetsky wrote:
> I'm trying to write tactics that are more complex than the basic
> constructs supported by Isar.
See the isar-ref manual about method_setup for some clues on this slightly
cumbersome task. Isar does not provide a separate language for definining
proof methods, everything needs to be done by hand via low-level ML
> In particular, I'd like to be able to use the ALLGOALS tactic.
In that case, there is probably no need to define new methods at all,
since most existing methods already do the right thing. E.g. use simp_all
for ALLGOALS asm_full_simp_tac, or blast+ for ALLGOALS blast_tac. Also
note that various tactic emulation methods (e.g. rule_tac) provide
explicit syntax for addressing goal ranges (again see the isar-ref
This archive was generated by a fusion of
Pipermail (Mailman edition) and