[isabelle] Renaming Tacticals



Hi

I have a series of methods to apply which looks something like this

apply (rule ((basic)+)?, ((conjL)+)?, ((disjR)+)?, ...)

Is there anyway that I can rename the above to something, say bigRule, so that

apply (rule bigRule)

executes the first line?  I had an attempt using ML as

ML {* fun PETER (basic, impR, impL, conjL, disjR, false, conjR, disjL) = REPEAT (EVERY [basic, impR, impL, conjL, disjR, false, conjR, disjL]); *}

but am having trouble (if this even works) in converting it to Isar.

Many thanks

Peter





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