X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.glade;h=fb585f50d262e489c2b65b41178ffcf374e59b61;hb=dcef667a444aa0f189225855c1433d26b65fb8b7;hp=2447b28817684fd33d0d5398ea3f38e055e09416;hpb=214b87039cc59cc6ecb5a54cf68b296b0a3ada92;p=helm.git

diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index 2447b2881..fb585f50d 100644
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -1022,6 +1022,15 @@
                                 <property name="use_underline">True</property>
                               </widget>
                             </child>
+                            <child>
+                              <widget class="GtkCheckMenuItem" id="menuitemAutoAltL">
+                                <property name="visible">True</property>
+                                <property name="tooltip" translatable="yes">Automatically expands TeX macros to their corresponding UTF-8 symbol</property>
+                                <property name="label" translatable="yes">Auto-expand TeX Macros</property>
+                                <property name="use_underline">True</property>
+                                <property name="active">True</property>
+                              </widget>
+                            </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="deleteMenuItem">
                                 <property name="visible">True</property>
@@ -1298,8 +1307,8 @@
                             <child>
                               <widget class="GtkImageMenuItem" id="showUnicodeTable">
                                 <property name="visible">True</property>
-                                <property name="tooltip" translatable="yes">Show the conversion table from TeX to UTF8</property>
-                                <property name="label" translatable="yes">Tex/UTF8 table</property>
+                                <property name="tooltip" translatable="yes">Show the conversion table from TeX like sequences to UTF-8</property>
+                                <property name="label" translatable="yes">TeX/UTF-8 table</property>
                                 <property name="use_underline">True</property>
                                 <child internal-child="image">
                                   <widget class="GtkImage" id="menu-item-image20">
@@ -1453,7 +1462,7 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Negaton (¬_i)</property>
+                                            <property name="label" translatable="yes">Negation (¬_i)</property>
                                             <property name="response_id">0</property>
                                           </widget>
                                           <packing>
@@ -1472,6 +1481,30 @@
                                             <property name="position">5</property>
                                           </packing>
                                         </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butForall_intro">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Universal (∀_i)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">6</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butExists_intro">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Existential (∃_i)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">7</property>
+                                          </packing>
+                                        </child>
                                       </widget>
                                     </child>
                                     <child>
@@ -1545,7 +1578,7 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Negaton (¬_e)</property>
+                                            <property name="label" translatable="yes">Negation (¬_e)</property>
                                             <property name="response_id">0</property>
                                           </widget>
                                           <packing>
@@ -1564,6 +1597,30 @@
                                             <property name="position">5</property>
                                           </packing>
                                         </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butForall_elim">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Universal (∀_e)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">6</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butExists_elim">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Existential (∃_e)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">7</property>
+                                          </packing>
+                                        </child>
                                       </widget>
                                     </child>
                                     <child>
@@ -1598,11 +1655,11 @@
                                           </widget>
                                         </child>
                                         <child>
-                                          <widget class="GtkButton" id="butStart">
+                                          <widget class="GtkButton" id="butUseLemma">
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Prove (to start)</property>
+                                            <property name="label" translatable="yes">Use lemma (lem)</property>
                                             <property name="response_id">0</property>
                                           </widget>
                                           <packing>
@@ -1614,7 +1671,7 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Discharge (discharge [  ])</property>
+                                            <property name="label" translatable="yes">Discharge (discharge)</property>
                                             <property name="response_id">0</property>
                                           </widget>
                                           <packing>