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 :-)


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