isabelle: src/HOL/Sledgehammer.thy@25c1ff13dbdb (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
54838 16511f84913c reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated) blanchet parents: 52641 diff changeset	16	lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
58481 62bc7c79212b made 'moura' tactic more powerful blanchet parents: 58074 diff changeset	17	by (erule contrapos_nn) (rule arg_cong)
54838 16511f84913c reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated) blanchet parents: 52641 diff changeset	18
70934 25c1ff13dbdb removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade) blanchet parents: 69605 diff changeset	19	ML_file \<open>Tools/ATP/atp_systems.ML\<close>
25c1ff13dbdb removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade) blanchet parents: 69605 diff changeset	20
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	21	ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	22	ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	23	ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	24	ML_file \<open>Tools/Sledgehammer/sledgehammer_proof_methods.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	25	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_annotate.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	26	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_proof.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	27	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_preplay.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	28	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_compress.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	29	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_minimize.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	30	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	31	ML_file \<open>Tools/Sledgehammer/sledgehammer_prover.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	32	ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_atp.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	33	ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_smt.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	34	ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_minimize.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	35	ML_file \<open>Tools/Sledgehammer/sledgehammer_mepo.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	36	ML_file \<open>Tools/Sledgehammer/sledgehammer_mash.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	37	ML_file \<open>Tools/Sledgehammer/sledgehammer.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	38	ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	39
70934 25c1ff13dbdb removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade) blanchet parents: 69605 diff changeset	40	lemma "1 + 1 = 2"
25c1ff13dbdb removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade) blanchet parents: 69605 diff changeset	41	sledgehammer [iprover, overlord, dont_minimize, dont_preplay]
25c1ff13dbdb removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade) blanchet parents: 69605 diff changeset	42
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	43	end

author	blanchet
	Fri, 25 Oct 2019 14:55:14 +0200
changeset 70934	25c1ff13dbdb
parent 69605	a96320074298
child 70944	849311b45428
permissions	-rw-r--r--