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");
(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#butUseLemma
+ (fun () -> source_buffer#insert "apply rule (lem …);\n");
connect_button main#butDischarge
- (fun () -> source_buffer#insert "apply rule (discharge […]).\n");
+ (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 *)