X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.glade;h=0d80fe22c933960827789de606e3c3601b392610;hb=5e72e41f4f86814e56d4b00959ccc56c71042a4c;hp=5e39120a92ea524f7a28fc96d821b39df5b314da;hpb=21da7b0b7cd14ebc928a84ca9f53793e3956dfb7;p=helm.git diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index 5e39120a9..0d80fe22c 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 @@ -1274,6 +1283,14 @@ True + + + True + Displays the database of hints + Hints database + True + + True @@ -1298,8 +1315,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 @@ -1387,6 +1404,7 @@ True + 2 True @@ -1396,13 +1414,390 @@ True - + + True + True + + + True + + + True + True + True + 0 + + + True + Implication (⇒<sub>i</sub>) + True + + + + + + + True + True + True + 0 + + + True + Conjunction (∧<sub>i</sub>) + True + + + + + 1 + + + + + True + True + True + 0 + + + True + Disjunction left (∨<sub>i-l</sub>) + True + + + + + 2 + + + + + True + True + True + 0 + + + True + Disjunction right (∨<sub>i-r</sub>) + True + + + + + 3 + + + + + True + True + True + 0 + + + True + Negation (¬<sub>i</sub>) + True + + + + + 4 + + + + + True + True + True + 0 + + + True + Top (⊤<sub>i</sub>) + True + + + + + 5 + + + + + True + True + True + 0 + + + True + Universal (∀<sub>i</sub>) + True + + + + + 6 + + + + + True + True + True + 0 + + + True + Existential (∃<sub>i</sub>) + True + + + + + 7 + + + + + + + True + Introduction rules + + + label_item + + + + + False + - + + True + True + + + True + + + True + True + True + 0 + + + True + Implication (⇒<sub>e</sub>) + True + + + + + + + True + True + True + 0 + + + True + Conjunction left (∧<sub>e-l</sub>) + True + + + + + 1 + + + + + True + True + True + 0 + + + True + Conjunction right (∧<sub>e-r</sub>) + True + + + + + 2 + + + + + True + True + True + 0 + + + True + Disjunction (∨<sub>e</sub>) + True + + + + + 3 + + + + + True + True + True + 0 + + + True + Negation (¬<sub>e</sub>) + True + + + + + 4 + + + + + True + True + True + 0 + + + True + Bottom (⊥<sub>e</sub>) + True + + + + + 5 + + + + + True + True + True + 0 + + + True + Universal (∀<sub>e</sub>) + True + + + + + 6 + + + + + True + True + True + 0 + + + True + Existential (∃<sub>e</sub>) + True + + + + + 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 +