Is there any way to get more information, why a proof method is not applicable?
I'm currently facing the following goal:
1. ⟦wf_graph G; wf_rule r; wf_cat CatGraph; dang r G m⟧ ⟹ ∃p. wf_pushout CatGraph p m m and I'm able to apply the following introduction rule
apply (rule exI[where x = "⦇pf' = (undefined, m, undefined), pg' = (undefined, m, undefined)⦈"]) but as soon as I start to replace one undefined with for example
G I get
Failed to apply proof method⌂:.
Still difficult for me to find these. Any reason they are not listed in the isar-ref PDF?
Robert Soeldner has marked this topic as resolved.
Last updated: Sep 25 2022 at 23:25 UTC