# Re: [isabelle] Creating simple tactics

Greg Bronevetsky wrote:

`I'm trying to write tactics that are more complex than the basic
``constructs supported by Isar. In particular, I'd like to be able to use
``the ALLGOALS tactic. The first thing I tried was embedding ML code into
``tactics like in the following example:
` apply(tactic {* Addsimps[Let_def]; ALLGOALS(Simp_tac) *})

`While more basic versions of the above seem to work, the above example
``does not. It appears that Simp_tac does not unfold my let definitions,
``meaning that my call to Addsimps[Let_def] fails to add Let_def to the
``simp set. Why not? How else would I do this?
`

Addsimps modifies the simpset associated with the current theory,
and Simp_tac uses it (as does simpset ()).
First point: Is the above really what you want, or rather
ALLGOALS (simp_tac (simpset () addsimps [Let_def])) ?
Second point:

`In translating Isabelle proofs into Isar I've found that things
``depending on the notion of the current theory are liable to misbehave
`(including what I've written above).
In Isar I would have to write (in place of my version above),
SIMPSET (fn ss => ALLGOALS (simp_tac (ss addsimps [Let_def]))).
See 10.2.3 of the reference manual.
However I have found in Isar that
ML {*
Addsimps [xxx] ;
*}
seems to work as expected.
Regards,
Jeremy

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