Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Sledgehammer.thy
changeset 82396 7230281bde03
parent 82360 6a09257afd06 
--- a/src/HOL/Sledgehammer.thy	Tue Apr 01 12:10:45 2025 +0200
+++ b/src/HOL/Sledgehammer.thy	Wed Apr 02 11:18:35 2025 +0200
@@ -7,7 +7,15 @@
 section \<open>Sledgehammer: Isabelle--ATP Linkup\<close>
 
 theory Sledgehammer
-imports Presburger SMT Try0_HOL
+  imports
+    \<comment> \<open>FIXME: \<^theory>\<open>HOL.Try0_HOL\<close> has to be imported first so that @{attribute try0_schedule} gets
+    the value assigned value there. Otherwise, the value is the one assigned in \<^theory>\<open>HOL.Try0\<close>,
+    which is imported transitively by both \<^theory>\<open>HOL.Presburger\<close> and \<^theory>\<open>HOL.SMT\<close>. It seems
+    that, when merging the attributes from two theories, the value assigned int the leftmost theory
+    has precedence.\<close>
+    Try0_HOL
+    Presburger
+    SMT
 keywords
   "sledgehammer" :: diag and
   "sledgehammer_params" :: thy_decl
isabelle