--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Sat Apr 25 09:48:06 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Sat Apr 25 20:49:26 2015 +0200
@@ -413,11 +413,12 @@
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
- val [provers_arg, isar_proofs_arg] = args
+ val [provers_arg, isar_proofs_arg, try0_arg] = args
val override_params =
((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
[("isar_proofs", [isar_proofs_arg]),
+ ("try0", [try0_arg]),
("blocking", ["true"]),
("debug", ["false"]),
("verbose", ["false"]),
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Apr 25 09:48:06 2015 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Apr 25 20:49:26 2015 +0200
@@ -73,7 +73,8 @@
private def clicked {
PIDE.options.string("sledgehammer_provers") = provers.getText
- sledgehammer.apply_query(List(provers.getText, isar_proofs.selected.toString))
+ sledgehammer.apply_query(
+ List(provers.getText, isar_proofs.selected.toString, try0.selected.toString))
}
private val provers_label = new Label("Provers:") {
@@ -103,10 +104,15 @@
}
private val isar_proofs = new CheckBox("Isar proofs") {
- tooltip = "Specify whether Isar proofs should be output in addition to metis line"
+ tooltip = "Specify whether Isar proofs should be output in addition to \"by\" one-liner"
selected = false
}
+ private val try0 = new CheckBox("Try methods") {
+ tooltip = "Try standard proof methods like \"auto\" and \"blast\" as alternatives to \"metis\""
+ selected = true
+ }
+
private val apply_query = new Button("<html><b>Apply</b></html>") {
tooltip = "Search for first-order proof using automatic theorem provers"
reactions += { case ButtonClicked(_) => clicked }
@@ -124,7 +130,7 @@
private val controls =
new Wrap_Panel(Wrap_Panel.Alignment.Right)(
- provers_label, Component.wrap(provers), isar_proofs,
+ provers_label, Component.wrap(provers), isar_proofs, try0,
process_indicator.component, apply_query, cancel_query, locate_query, zoom)
add(controls.peer, BorderLayout.NORTH)