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:

  src/Pure/meta_simplifier.ML
  src/Provers/classical.ML
  src/Provers/clasimp.ML


	Makarius





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