X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.glade;h=fb585f50d262e489c2b65b41178ffcf374e59b61;hb=4446f96e1829f1a82fc71cb49d8ddc392e73b155;hp=34121dd9f9d651ea5fe45465818dadd562033847;hpb=65aa5d46b240da7b91e57fc74890d8544aa479c3;p=helm.git diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index 34121dd9f..fb585f50d 100644 --- a/helm/software/matita/matita.glade +++ b/helm/software/matita/matita.glade @@ -11,7 +11,6 @@ 500 480 True - MainWin True @@ -1023,6 +1022,15 @@ True + + + True + Automatically expands TeX macros to their corresponding UTF-8 symbol + Auto-expand TeX Macros + True + True + + True @@ -1161,15 +1169,6 @@ True - - - True - Show _tactics bar - True - True - - - True @@ -1191,6 +1190,15 @@ + + + True + Shows a palette with natural deduction rules + Natural deduction palette + True + + + True @@ -1299,8 +1307,8 @@ True - Show the conversion table from TeX to UTF8 - Tex/UTF8 table + Show the conversion table from TeX like sequences to UTF-8 + TeX/UTF-8 table True @@ -1388,6 +1396,7 @@ True + 2 True @@ -1397,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 +