]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/matita.glade
rules fixed
[helm.git] / helm / software / matita / matita.glade
index 5e39120a92ea524f7a28fc96d821b39df5b314da..2447b28817684fd33d0d5398ea3f38e055e09416 100644 (file)
                         <property name="use_underline">True</property>
                         <child>
                           <widget class="GtkMenu" id="viewMenu_menu">
-                            <child>
-                              <widget class="GtkCheckMenuItem" id="tacticsBarMenuItem">
-                                <property name="visible">True</property>
-                                <property name="label" translatable="yes">Show _tactics bar</property>
-                                <property name="use_underline">True</property>
-                                <property name="active">True</property>
-                                <accelerator key="F2" modifiers="" signal="activate"/>
-                              </widget>
-                            </child>
                             <child>
                               <widget class="GtkMenuItem" id="newCicBrowserMenuItem">
                                 <property name="visible">True</property>
                                 <accelerator key="F11" modifiers="" signal="activate"/>
                               </widget>
                             </child>
+                            <child>
+                              <widget class="GtkCheckMenuItem" id="menuitemPalette">
+                                <property name="visible">True</property>
+                                <property name="tooltip" translatable="yes">Shows a palette with natural deduction rules</property>
+                                <property name="label" translatable="yes">Natural deduction palette</property>
+                                <property name="use_underline">True</property>
+                                <accelerator key="F2" modifiers="" signal="activate"/>
+                              </widget>
+                            </child>
                             <child>
                               <widget class="GtkSeparatorMenuItem" id="separator1">
                                 <property name="visible">True</property>
                     <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>
                               <widget class="GtkVBox" id="vboxTacticsPalette">
                                 <property name="visible">True</property>
                                 <child>
-                                  <placeholder/>
+                                  <widget class="GtkExpander" id="expander1">
+                                    <property name="visible">True</property>
+                                    <property name="can_focus">True</property>
+                                    <child>
+                                      <widget class="GtkVBox" id="vbox1">
+                                        <property name="visible">True</property>
+                                        <child>
+                                          <widget class="GtkButton" id="butImpl_intro">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Implication (⇒_i)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butAnd_intro">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Conjunction (∧_i)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">1</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butOr_intro_left">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Disjunction left (∨_i_l)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">2</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butOr_intro_right">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Disjunction right (∨_i_r)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">3</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butNot_intro">
+                                            <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="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">4</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butTop_intro">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Top (⊤_i)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">5</property>
+                                          </packing>
+                                        </child>
+                                      </widget>
+                                    </child>
+                                    <child>
+                                      <widget class="GtkLabel" id="label4">
+                                        <property name="visible">True</property>
+                                        <property name="label" translatable="yes">Introduction rules</property>
+                                      </widget>
+                                      <packing>
+                                        <property name="type">label_item</property>
+                                      </packing>
+                                    </child>
+                                  </widget>
+                                  <packing>
+                                    <property name="expand">False</property>
+                                  </packing>
                                 </child>
                                 <child>
-                                  <placeholder/>
+                                  <widget class="GtkExpander" id="expander2">
+                                    <property name="visible">True</property>
+                                    <property name="can_focus">True</property>
+                                    <child>
+                                      <widget class="GtkVBox" id="vbox3">
+                                        <property name="visible">True</property>
+                                        <child>
+                                          <widget class="GtkButton" id="butImpl_elim">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Implication (⇒_e)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butAnd_elim_left">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Conjunction left (∧_e_l)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">1</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butAnd_elim_right">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Conjunction right (∧_e_r)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">2</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butOr_elim">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Disjunction (∨_e)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">3</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butNot_elim">
+                                            <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="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">4</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butBot_elim">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Bottom (⊥_e)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">5</property>
+                                          </packing>
+                                        </child>
+                                      </widget>
+                                    </child>
+                                    <child>
+                                      <widget class="GtkLabel" id="label5">
+                                        <property name="visible">True</property>
+                                        <property name="label" translatable="yes">Elimination rules</property>
+                                      </widget>
+                                      <packing>
+                                        <property name="type">label_item</property>
+                                      </packing>
+                                    </child>
+                                  </widget>
+                                  <packing>
+                                    <property name="expand">False</property>
+                                    <property name="position">1</property>
+                                  </packing>
                                 </child>
                                 <child>
-                                  <placeholder/>
+                                  <widget class="GtkExpander" id="expander3">
+                                    <property name="visible">True</property>
+                                    <property name="can_focus">True</property>
+                                    <child>
+                                      <widget class="GtkVBox" id="vbox4">
+                                        <property name="visible">True</property>
+                                        <child>
+                                          <widget class="GtkButton" id="butRAA">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Reduction to Absurdity (RAA)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butStart">
+                                            <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="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>
+                                      <widget class="GtkLabel" id="label6">
+                                        <property name="visible">True</property>
+                                        <property name="label" translatable="yes">Misc rules</property>
+                                      </widget>
+                                      <packing>
+                                        <property name="type">label_item</property>
+                                      </packing>
+                                    </child>
+                                  </widget>
+                                  <packing>
+                                    <property name="expand">False</property>
+                                    <property name="position">2</property>
+                                  </packing>
                                 </child>
                               </widget>
                             </child>