Re: [isabelle] Augmenting facts

On Wed, 29 Sep 2010, John Munroe wrote:

Just some further information: I'd like to apply the auto_tac with additional facts.

Maybe you actually want to augment the clasimpset context of auto_tac, which is actually a pair over claset * simpset. There are various ML operators for that, such as addIs or addsimps; see the infix declarations at the start of the following source files:



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