isabelle: src/HOL/Sledgehammer.thy@f3c4849868b8 (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: Fabian Immler, TU Muenchen
2f8fb5242799 more Sledgehammer refactoring blanchet parents: 35827 diff changeset	5	Author: Jasmin Blanchette, TU Muenchen
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	6	*)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	7
35827 f552152d7747 renamed "ATP_Linkup" theory to "Sledgehammer" blanchet parents: 35826 diff changeset	8	header {* Sledgehammer: Isabelle--ATP Linkup *}
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	9
35827 f552152d7747 renamed "ATP_Linkup" theory to "Sledgehammer" blanchet parents: 35826 diff changeset	10	theory Sledgehammer
39946 78faa9b31202 move Metis into Plain blanchet parents: 39942 diff changeset	11	imports Plain
39947 f95834c8bb4d tuning blanchet parents: 39946 diff changeset	12	uses "Tools/ATP/atp_problem.ML"
f95834c8bb4d tuning blanchet parents: 39946 diff changeset	13	"Tools/ATP/atp_proof.ML"
f95834c8bb4d tuning blanchet parents: 39946 diff changeset	14	"Tools/ATP/atp_systems.ML"
f95834c8bb4d tuning blanchet parents: 39946 diff changeset	15	"Tools/Sledgehammer/sledgehammer_util.ML"
f95834c8bb4d tuning blanchet parents: 39946 diff changeset	16	"Tools/Sledgehammer/sledgehammer_filter.ML"
f95834c8bb4d tuning blanchet parents: 39946 diff changeset	17	"Tools/Sledgehammer/sledgehammer_translate.ML"
f95834c8bb4d tuning blanchet parents: 39946 diff changeset	18	"Tools/Sledgehammer/sledgehammer_reconstruct.ML"
f95834c8bb4d tuning blanchet parents: 39946 diff changeset	19	"Tools/Sledgehammer/sledgehammer.ML"
f95834c8bb4d tuning blanchet parents: 39946 diff changeset	20	"Tools/Sledgehammer/sledgehammer_minimize.ML"
f95834c8bb4d tuning blanchet parents: 39946 diff changeset	21	"Tools/Sledgehammer/sledgehammer_isar.ML"
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
39947 f95834c8bb4d tuning blanchet parents: 39946 diff changeset	24	setup {*
f95834c8bb4d tuning blanchet parents: 39946 diff changeset	25	ATP_Systems.setup
f95834c8bb4d tuning blanchet parents: 39946 diff changeset	26	#> Sledgehammer.setup
f95834c8bb4d tuning blanchet parents: 39946 diff changeset	27	#> Sledgehammer_Isar.setup
f95834c8bb4d tuning blanchet parents: 39946 diff changeset	28	*}
23444 6d4703843f93 added Metis setup (from Metis.thy); wenzelm parents: 21999 diff changeset	29
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	30	end

author	blanchet
	Tue, 05 Oct 2010 10:59:12 +0200
changeset 39950	f3c4849868b8
parent 39947	f95834c8bb4d
child 39951	ff60a6e4edfe
permissions	-rw-r--r--