Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
skip &&& goals
authornipkow
Fri, 18 Sep 2009 14:40:06 +0200
changeset 32607 e7fe01b74a92
parent 32599 979c274089a5
child 32608 c0056c2c1d17
skip &&& goals
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 17 19:13:22 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Sep 18 14:40:06 2009 +0200
@@ -396,7 +396,9 @@
     |> log o prefix (metis_tag id) 
   end
 
-fun sledgehammer_action args id (st as {log, ...}: Mirabelle.run_args) =
+fun sledgehammer_action args id (st as {log, pre, ...}: Mirabelle.run_args) =
+  if can Logic.dest_conjunction (Thm.major_prem_of(snd(snd(Proof.get_goal pre))))
+  then () else
   let
     val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_time,
         inc_metis_timeout, inc_metis_lemmas, inc_metis_posns)
isabelle