# HG changeset patch # User wenzelm # Date 1429987766 -7200 # Node ID a95023a21725220b3789b1c7d3736e16a858d6b2 # Parent 90e88e521e0e3de914ab48bf889e88d4afc828dd added checkbox for try0; diff -r 90e88e521e0e -r a95023a21725 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- 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"]), diff -r 90e88e521e0e -r a95023a21725 src/Tools/jEdit/src/sledgehammer_dockable.scala --- 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("Apply") { 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)