# Re: [isabelle] 2 questions

Ola´ Francisco, nice to hear from you again,
> a) In some of those logics an upper bound on the number of applications
> of non-safe rules (i.e. BoxLeft) can be found depending on the
> complexity of the formula to be established (or not establised). To
> represente this an ML-function has to be written that calculates the
> complexity of the formula (easy). However it is not clear to me how I
> can write a tactic looking like
> *REPEAT_DETERM_N* (complexity ??formula??)
Isn't the SUBGOAL tactical (see reference manual) what you need?
Something like
SUBGOAL (fn (t, i)=> REPEAT_DETERM_N (complexity t) your_tactic)
should do what you need...
I leave "b)" to someone else :-)
Alex

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