Re: [isabelle] Giving a name to a tactics-expression



On Thu, 18 Feb 2010, Peter Lammich wrote:

Trying to translate it to ML, I cannot find any ML-tactics equivalent for "erule (1)". There is only etac, but this seems to have no number of additional premises.

The numbers merely specify additional assumption steps -- which used to be a very common idiom in old-style tactic scripts. (In Isar, reasoning by assumption is usually implicit in the proof structure, e.g. after closing a 'by'.)

The low-level tactic is called assume_tac.


	Makarius





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