X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=8bc226ed4a4bdbbbf33292d7afaa3a4f75c6f406;hb=424982ded255df68245241f56064202844ed1194;hp=84909e95bd99d12738cec8c54f1e1fcac128ea36;hpb=5c6d665243a131e00b53e80b09250e3e1cb19cff;p=helm.git

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 84909e95b..8bc226ed4 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -791,8 +791,20 @@ class gui () =
         (fun () -> source_buffer#insert "apply rule (⊥_e (…));\n");
       connect_button main#butRAA
         (fun () -> source_buffer#insert "apply rule (RAA […] (…));\n");
+      connect_button main#butUseLemma
+        (fun () -> source_buffer#insert "apply rule (lem …);\n");
       connect_button main#butDischarge
         (fun () -> source_buffer#insert "apply rule (discharge […]);\n");
+      
+      connect_button main#butForall_intro
+        (fun () -> source_buffer#insert "apply rule (∀_i {…} (…));\n");
+      connect_button main#butForall_elim
+        (fun () -> source_buffer#insert "apply rule (∀_e {…} (…));\n");
+      connect_button main#butExists_intro
+        (fun () -> source_buffer#insert "apply rule (∃_i {…} (…));\n");
+      connect_button main#butExists_elim
+        (fun () -> source_buffer#insert 
+          "apply rule (∃_e (…) {…} […] (…));\n\t[\n\t|\n\t]\n");
 
     
       (* TO BE REMOVED *)