X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.glade;h=0d80fe22c933960827789de606e3c3601b392610;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hp=34121dd9f9d651ea5fe45465818dadd562033847;hpb=65aa5d46b240da7b91e57fc74890d8544aa479c3;p=helm.git diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index 34121dd9f..0d80fe22c 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 @@ -1275,6 +1283,14 @@ True + + + True + Displays the database of hints + Hints database + True + + True @@ -1299,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 @@ -1388,6 +1404,7 @@ True + 2 True @@ -1397,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 +