Fad*_*oua 5 isabelle
如何更改规则中的前提顺序？例如,在伊莎贝尔的自然演绎规则中:
mp: ?P ? ?Q ? ?P ? ?Q
我们可以将订单更改为:
?P ? ?P ? ?Q ? ?Q
我可以使用rev_mp或定义一个新的引理,但我要找的是是否有一个定理修饰符改变了前提的顺序.
rev_mp
And*_*ler 5
定理的前提可以随属性一起旋转rotated.您还可以指定要旋转的场所数量,例如mp[rotated 1].AFAIK没有任何属性可以随意排列场地.
rotated
mp[rotated 1]
归档时间：
9 年，4 月 前
查看次数：
109 次
最近记录：