apply rule (lem EM) works

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

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 84909e95bd99d12738cec8c54f1e1fcac128ea36..db26ba20a55d7575e54f6b9932e5c0d71aa1404e 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -791,6 +791,8 @@ 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");