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.
no need for "eq" facts -- good old "=" is good enough for us
authorblanchet
Mon, 23 Aug 2010 18:04:31 +0200
changeset 38681 f9edc593e929
parent 38680 634a6d400c2e
child 38682 3a203da3f89b
no need for "eq" facts -- good old "=" is good enough for us
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 17:53:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 18:04:31 2010 +0200
@@ -386,7 +386,7 @@
 (* FIXME: put other record thms here, or declare as "no_atp" *)
 val multi_base_blacklist =
   ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
-   "split_asm", "cases", "ext_cases"]
+   "split_asm", "cases", "ext_cases", "eq"]
 
 val max_lambda_nesting = 3
isabelle