Jan van Brügge (Sep 03 2024 at 14:11): Jan van Brügge (Sep 03 2024 at 14:11):frule in isabelle is similar to drule, except that the original assumption kept. Is there a similar tactic for elim rules? I really need to use biresolution (ie erule) because of a higher order match in the goal, but I need the assumption still afterwards.
Jan van Brügge (Sep 03 2024 at 14:16):So given a rule A ==> B ==> C and a goal D ==> A ==> C I want to get the goal D ==> A ==> B, where erule would result in D ==> B
Last updated: Nov 16 2025 at 20:22 UTC