commented out unfinished proof

[helm.git] / helm / software / matita / matitaGui.ml

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 393da7cef0e118b5307fd513482e354ea32aed20..db26ba20a55d7575e54f6b9932e5c0d71aa1404e 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -791,8 +791,11 @@ 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#butStart
-        (fun () -> source_buffer#insert "apply rule (prove (…));\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");
+
     
       (* TO BE REMOVED *)
       main#scriptNotebook#remove_page 1;