The order of premises
isabelle
Solution
The premises of a theorem can be rotated with the attribute `rotated`. You can also specify the number of premises to rotate, e.g., `mp[rotated 1]`. AFAIK there's no attribute for arbitrarily permuting the premises.
Problem
How to change the order of premises in a rule? For instance, in Isabelle's natural deduction rule: ``` mp: ?P ⟶ ?Q ⟹ ?P ⟹ ?Q ``` Can we change the order to: ``` ?P ⟹ ?P ⟶ ?Q ⟹ ?Q ``` I can use `rev_mp` or define a new lemma, but what I am looking for is whether there is a theorem modifier that changes the order of premises.