Re: [isabelle] Giving a name to a tactics-expression
Peter Lammich wrote:
Peter Lammich schrieb:
Is there a way to give a short name to a complex tactic-expression. I
have, e.g., the following pattern that I frequently use.
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
apply (((erule (1) lemma1)+)?,erule lemma2,simp)+
I was under the impression that erule (1) was just (erule,assumption)
which then would translate to "etac some_rule THEN' atac" in ML.
In any case, check out Christian's example from the Isabelle Developer
Workshop, where he shows an example translation from apply-style proof
script to ML method: http://tphols.in.tum.de/IDW/CU-Ex1.thy
And also look at Makarius's slides/examples on proof methods. Available
I've found these practical examples have helped me much more than the
reference manual. Once I understood what the point of the exercise was,
the reference manual started to help instead of confuse.
This archive was generated by a fusion of
Pipermail (Mailman edition) and