Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Renaming Tacticals

view this post on Zulip Email Gateway (Aug 18 2022 at 10:17):

From: Peter Chapman <pc@cs.st-and.ac.uk>
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

Last updated: Nov 21 2024 at 12:39 UTC