isabelle: src/HOL/Sledgehammer.thy@da14e77a48b2 (annotated)

35827 f552152d7747 renamed "ATP_Linkup" theory to "Sledgehammer" blanchet parents: 35826 diff changeset	1	(* Title: HOL/Sledgehammer.thy
38027 505657ddb047 standardize "Author" tags blanchet parents: 38025 diff changeset	2	Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
38028 22dcaec5fa77 minor refactoring blanchet parents: 38027 diff changeset	3	Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
35865 2f8fb5242799 more Sledgehammer refactoring blanchet parents: 35827 diff changeset	4	Author: Jasmin Blanchette, TU Muenchen
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	5	*)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	6
60758 d8d85a8172b5 isabelle update_cartouches; wenzelm parents: 59471 diff changeset	7	section \<open>Sledgehammer: Isabelle--ATP Linkup\<close>
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	8
35827 f552152d7747 renamed "ATP_Linkup" theory to "Sledgehammer" blanchet parents: 35826 diff changeset	9	theory Sledgehammer
82396 7230281bde03 added a user-configurable schedule to try0 desharna parents: 82360 diff changeset	10	imports
7230281bde03 added a user-configurable schedule to try0 desharna parents: 82360 diff changeset	11	\<comment> \<open>FIXME: \<^theory>\<open>HOL.Try0_HOL\<close> has to be imported first so that @{attribute try0_schedule} gets
7230281bde03 added a user-configurable schedule to try0 desharna parents: 82360 diff changeset	12	the value assigned value there. Otherwise, the value is the one assigned in \<^theory>\<open>HOL.Try0\<close>,
7230281bde03 added a user-configurable schedule to try0 desharna parents: 82360 diff changeset	13	which is imported transitively by both \<^theory>\<open>HOL.Presburger\<close> and \<^theory>\<open>HOL.SMT\<close>. It seems
7230281bde03 added a user-configurable schedule to try0 desharna parents: 82360 diff changeset	14	that, when merging the attributes from two theories, the value assigned int the leftmost theory
7230281bde03 added a user-configurable schedule to try0 desharna parents: 82360 diff changeset	15	has precedence.\<close>
7230281bde03 added a user-configurable schedule to try0 desharna parents: 82360 diff changeset	16	Try0_HOL
7230281bde03 added a user-configurable schedule to try0 desharna parents: 82360 diff changeset	17	Presburger
7230281bde03 added a user-configurable schedule to try0 desharna parents: 82360 diff changeset	18	SMT
63432 ba7901e94e7b tuned; wenzelm parents: 60758 diff changeset	19	keywords
ba7901e94e7b tuned; wenzelm parents: 60758 diff changeset	20	"sledgehammer" :: diag and
ba7901e94e7b tuned; wenzelm parents: 60758 diff changeset	21	"sledgehammer_params" :: thy_decl
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	22	begin
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	23
73418 7d7d959547a1 support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl); wenzelm parents: 72593 diff changeset	24	ML_file \<open>Tools/ATP/system_on_tptp.ML\<close>
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	25	ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	26	ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	27	ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	28	ML_file \<open>Tools/Sledgehammer/sledgehammer_proof_methods.ML\<close>
81254 d3c0734059ee variable instantiation in Sledgehammer and Metis blanchet parents: 77670 diff changeset	29	ML_file \<open>Tools/Sledgehammer/sledgehammer_instantiations.ML\<close>
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	30	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_annotate.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	31	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_proof.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	32	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_preplay.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	33	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_compress.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	34	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_minimize.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	35	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar.ML\<close>
72400 abfeed05c323 tune filename desharna parents: 72342 diff changeset	36	ML_file \<open>Tools/Sledgehammer/sledgehammer_atp_systems.ML\<close>
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	37	ML_file \<open>Tools/Sledgehammer/sledgehammer_prover.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	38	ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_atp.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	39	ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_smt.ML\<close>
82202 a1f85f579a07 initial work on Magnushammer-inspured tactic hammer (from Jasmin) desharna parents: 81254 diff changeset	40	ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_tactic.ML\<close>
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	41	ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_minimize.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	42	ML_file \<open>Tools/Sledgehammer/sledgehammer_mepo.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	43	ML_file \<open>Tools/Sledgehammer/sledgehammer_mash.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	44	ML_file \<open>Tools/Sledgehammer/sledgehammer.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	45	ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
73684 a63d76ba0a03 avoid duplicate loading of ML file; wenzelm parents: 73418 diff changeset	46	ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close>
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	47
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	48	end

author	Manuel Eberl <manuel@pruvisto.org>
	Tue, 15 Apr 2025 17:38:20 +0200
changeset 82518	da14e77a48b2
parent 82396	7230281bde03
permissions	-rw-r--r--