raise uncertain when a sort is not a sort but may be, use max for mixing universes...

[helm.git] / helm / software / matita / matita.glade

diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index 2b239b4e5485ea3cd93a969023145bd85ca3c6f9..4739e14f80ee6a30c4688776d99699bb5a7b16de 100644 (file)
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -1387,6 +1387,7 @@
                     <child>
                       <widget class="GtkHBox" id="hbox18">
                         <property name="visible">True</property>
+                        <property name="spacing">2</property>
                         <child>
                           <widget class="GtkHandleBox" id="TacticsButtonsHandlebox">
                             <property name="visible">True</property>
@@ -1452,7 +1453,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>
@@ -1471,6 +1472,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>
@@ -1544,7 +1569,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>
@@ -1563,6 +1588,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>
@@ -1597,17 +1646,29 @@
                                           </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>
                                             <property name="position">1</property>
                                           </packing>
                                         </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butDischarge">
+                                            <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="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">2</property>
+                                          </packing>
+                                        </child>
                                       </widget>
                                     </child>
                                     <child>