From 5c6d665243a131e00b53e80b09250e3e1cb19cff Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 15 Nov 2008 15:32:59 +0000
Subject: [PATCH] no more prove in palette

---
 helm/software/matita/matita.glade | 12 ------------
 helm/software/matita/matitaGui.ml | 22 ++++++++++------------
 2 files changed, 10 insertions(+), 24 deletions(-)

diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index d33743eda..62eefcfd7 100644
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -1597,18 +1597,6 @@
                                             <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>
diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 6acf7357a..84909e95b 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -762,25 +762,25 @@ class gui () =
           else main#tacticsButtonsHandlebox#misc#hide ())
         ~check:main#menuitemPalette;
       connect_button main#butImpl_intro
-        (fun () -> source_buffer#insert "apply rule (⇒_i […] (…)).\n");
+        (fun () -> source_buffer#insert "apply rule (⇒_i […] (…));\n");
       connect_button main#butAnd_intro
         (fun () -> source_buffer#insert 
           "apply rule (∧_i (…) (…));\n\t[\n\t|\n\t]\n");
       connect_button main#butOr_intro_left
-        (fun () -> source_buffer#insert "apply rule (∨_i_l (…)).\n");
+        (fun () -> source_buffer#insert "apply rule (∨_i_l (…));\n");
       connect_button main#butOr_intro_right
-        (fun () -> source_buffer#insert "apply rule (∨_i_r (…)).\n");
+        (fun () -> source_buffer#insert "apply rule (∨_i_r (…));\n");
       connect_button main#butNot_intro
-        (fun () -> source_buffer#insert "apply rule (¬_i […] (…)).\n");
+        (fun () -> source_buffer#insert "apply rule (¬_i […] (…));\n");
       connect_button main#butTop_intro
-        (fun () -> source_buffer#insert "apply rule (⊤_i).\n");
+        (fun () -> source_buffer#insert "apply rule (⊤_i);\n");
       connect_button main#butImpl_elim
         (fun () -> source_buffer#insert 
           "apply rule (⇒_e (…) (…));\n\t[\n\t|\n\t]\n");
       connect_button main#butAnd_elim_left
-        (fun () -> source_buffer#insert "apply rule (∧_e_l (…)).\n");
+        (fun () -> source_buffer#insert "apply rule (∧_e_l (…));\n");
       connect_button main#butAnd_elim_right
-        (fun () -> source_buffer#insert "apply rule (∧_e_r (…)).\n");
+        (fun () -> source_buffer#insert "apply rule (∧_e_r (…));\n");
       connect_button main#butOr_elim
         (fun () -> source_buffer#insert 
           "apply rule (∨_e (…) […] (…) […] (…));\n\t[\n\t|\n\t|\n\t]\n");
@@ -788,13 +788,11 @@ class gui () =
         (fun () -> source_buffer#insert 
           "apply rule (¬_e (…) (…));\n\t[\n\t|\n\t]\n");
       connect_button main#butBot_elim
-        (fun () -> source_buffer#insert "apply rule (⊥_e (…)).\n");
+        (fun () -> source_buffer#insert "apply rule (⊥_e (…));\n");
       connect_button main#butRAA
-        (fun () -> source_buffer#insert "apply rule (RAA […] (…)).\n");
-      connect_button main#butStart
-        (fun () -> source_buffer#insert "apply rule (prove (…)).\n");
+        (fun () -> source_buffer#insert "apply rule (RAA […] (…));\n");
       connect_button main#butDischarge
-        (fun () -> source_buffer#insert "apply rule (discharge […]).\n");
+        (fun () -> source_buffer#insert "apply rule (discharge […]);\n");
 
     
       (* TO BE REMOVED *)
-- 
2.39.2