isabelle: src/HOL/Sledgehammer.thy@0856026e2c88 (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
58061 3d060f43accb renamed new SMT module from 'SMT2' to 'SMT' blanchet parents: 57266 diff changeset	10	imports Presburger SMT
63432 ba7901e94e7b tuned; wenzelm parents: 60758 diff changeset	11	keywords
ba7901e94e7b tuned; wenzelm parents: 60758 diff changeset	12	"sledgehammer" :: diag and
ba7901e94e7b tuned; wenzelm parents: 60758 diff changeset	13	"sledgehammer_params" :: thy_decl
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	14	begin
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	15
73418 7d7d959547a1 support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl); wenzelm parents: 72593 diff changeset	16	ML_file \<open>Tools/ATP/system_on_tptp.ML\<close>
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	17	ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	18	ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	19	ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	20	ML_file \<open>Tools/Sledgehammer/sledgehammer_proof_methods.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	21	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_annotate.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	22	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_proof.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	23	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_preplay.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	24	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_compress.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	25	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_minimize.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	26	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar.ML\<close>
72400 abfeed05c323 tune filename desharna parents: 72342 diff changeset	27	ML_file \<open>Tools/Sledgehammer/sledgehammer_atp_systems.ML\<close>
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	28	ML_file \<open>Tools/Sledgehammer/sledgehammer_prover.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	29	ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_atp.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	30	ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_smt.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	31	ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_minimize.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	32	ML_file \<open>Tools/Sledgehammer/sledgehammer_mepo.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	33	ML_file \<open>Tools/Sledgehammer/sledgehammer_mash.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	34	ML_file \<open>Tools/Sledgehammer/sledgehammer.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	35	ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
73684 a63d76ba0a03 avoid duplicate loading of ML file; wenzelm parents: 73418 diff changeset	36	ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close>
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	37
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	38	end

author	wenzelm
	Tue, 23 Jan 2024 12:28:35 +0100
changeset 79517	0856026e2c88
parent 77670	b9e9b818d7b0
child 81254	d3c0734059ee
permissions	-rw-r--r--