Я написал это правило:
method rule_inversion uses P =
(cases rule: nt_network[OF P])
, но Изабель говорит мне
Rule has fewer premises than arguments given
Точное nt_network, похоже, не имеет значения, поскольку это не так:
method rule_inversion uses R P =
(cases rule: R[OF P])
Как применить OF P к правилу, используемому для cases внутри Eisbach, когда P является параметром tacti c?