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.
bring Sledgehammer's combinators in line with Metis's;
authorblanchet
Mon, 30 Aug 2010 08:53:27 +0200
changeset 38890 fd803530e8a0
parent 38889 d0e3f68dde63
child 38891 6e47e54214b8
bring Sledgehammer's combinators in line with Metis's; cf. email from Larry
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Aug 27 18:04:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Aug 30 08:53:27 2010 +0200
@@ -218,8 +218,10 @@
   count_combformula combformula
 
 val optional_helpers =
-  [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
-   (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
+  [(["c_COMBI"], @{thms COMBI_def}),
+   (["c_COMBK"], @{thms COMBK_def}),
+   (["c_COMBB"], @{thms COMBB_def}),
+   (["c_COMBC"], @{thms COMBC_def}),
    (["c_COMBS"], @{thms COMBS_def})]
 val optional_typed_helpers =
   [(["c_True", "c_False", "c_If"], @{thms True_or_False}),
isabelle