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


> 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 
manual).


	Makarius





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