X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.glade;h=2b239b4e5485ea3cd93a969023145bd85ca3c6f9;hb=88f24d23df67d88bf98c2ca32ac0d9854f3d9b00;hp=5e39120a92ea524f7a28fc96d821b39df5b314da;hpb=d5216e897267e4495290ecbf08eb9f88f6815a0c;p=helm.git diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index 5e39120a9..2b239b4e5 100644 --- a/helm/software/matita/matita.glade +++ b/helm/software/matita/matita.glade @@ -1160,15 +1160,6 @@ True - - - True - Show _tactics bar - True - True - - - True @@ -1190,6 +1181,15 @@ + + + True + Shows a palette with natural deduction rules + Natural deduction palette + True + + + True @@ -1396,13 +1396,234 @@ True - + + True + True + + + True + + + True + True + True + Implication (⇒_i) + 0 + + + + + True + True + True + Conjunction (∧_i) + 0 + + + 1 + + + + + True + True + True + Disjunction left (∨_i_l) + 0 + + + 2 + + + + + True + True + True + Disjunction right (∨_i_r) + 0 + + + 3 + + + + + True + True + True + Negaton (¬_i) + 0 + + + 4 + + + + + True + True + True + Top (⊤_i) + 0 + + + 5 + + + + + + + True + Introduction rules + + + label_item + + + + + False + - + + True + True + + + True + + + True + True + True + Implication (⇒_e) + 0 + + + + + True + True + True + Conjunction left (∧_e_l) + 0 + + + 1 + + + + + True + True + True + Conjunction right (∧_e_r) + 0 + + + 2 + + + + + True + True + True + Disjunction (∨_e) + 0 + + + 3 + + + + + True + True + True + Negaton (¬_e) + 0 + + + 4 + + + + + True + True + True + Bottom (⊥_e) + 0 + + + 5 + + + + + + + True + Elimination rules + + + label_item + + + + + False + 1 + - + + True + True + + + True + + + True + True + True + Reduction to Absurdity (RAA) + 0 + + + + + True + True + True + Prove (to start) + 0 + + + 1 + + + + + + + True + Misc rules + + + label_item + + + + + False + 2 + @@ -2116,59 +2337,6 @@ 3 2 5 - - - True - 0 - Find: - - - - - - - - - True - 0 - Replace with: - - - 1 - 2 - - - - - - - True - True - True - True - True - * - - - 1 - 2 - - - - - - True - True - * - - - 1 - 2 - 1 - 2 - - - True @@ -2267,6 +2435,59 @@ 5 + + + True + True + * + + + 1 + 2 + 1 + 2 + + + + + + True + True + True + True + True + * + + + 1 + 2 + + + + + + True + 0 + Replace with: + + + 1 + 2 + + + + + + + True + 0 + Find: + + + + + +