X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.glade;h=11a7321d6e7a39cbb200a6b01b146916c0050f92;hb=3969d815396a22dca5e71c5f85fa3ec66d79849e;hp=5e39120a92ea524f7a28fc96d821b39df5b314da;hpb=21da7b0b7cd14ebc928a84ca9f53793e3956dfb7;p=helm.git diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index 5e39120a9..11a7321d6 100644 --- a/helm/software/matita/matita.glade +++ b/helm/software/matita/matita.glade @@ -1022,6 +1022,15 @@ True + + + True + Automatically expands TeX macros to their corresponding UTF-8 symbol + Auto-expand TeX Macros + True + True + + True @@ -1160,15 +1169,6 @@ True - - - True - Show _tactics bar - True - True - - - True @@ -1190,6 +1190,15 @@ + + + True + Shows a palette with natural deduction rules + Natural deduction palette + True + + + True @@ -1387,6 +1396,7 @@ True + 2 True @@ -1396,13 +1406,294 @@ 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 + Negation (¬_i) + 0 + + + 4 + + + + + True + True + True + Top (⊤_i) + 0 + + + 5 + + + + + True + True + True + Universal (∀_i) + 0 + + + 6 + + + + + True + True + True + Existential (∃_i) + 0 + + + 7 + + + + + + + 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 + Negation (¬_e) + 0 + + + 4 + + + + + True + True + True + Bottom (⊥_e) + 0 + + + 5 + + + + + True + True + True + Universal (∀_e) + 0 + + + 6 + + + + + True + True + True + Existential (∃_e) + 0 + + + 7 + + + + + + + True + Elimination rules + + + label_item + + + + + False + 1 + - + + True + True + + + True + + + True + True + True + Reduction to Absurdity (RAA) + 0 + + + + + True + True + True + Use lemma (lem) + 0 + + + 1 + + + + + True + True + True + Discharge (discharge) + 0 + + + 2 + + + + + + + True + Misc rules + + + label_item + + + + + False + 2 +