isabelle: src/HOL/Sledgehammer.thy@cbcccf2a0f6f (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
35827 f552152d7747 renamed "ATP_Linkup" theory to "Sledgehammer" blanchet parents: 35826 diff changeset	7	header {* Sledgehammer: Isabelle--ATP Linkup *}
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
40181 3788b7adab36 integrated "smt" proof method with Sledgehammer blanchet parents: 40178 diff changeset	10	imports ATP SMT
46950 d0181abdbdac declare command keywords via theory header, including strict checking outside Pure; wenzelm parents: 43085 diff changeset	11	keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	12	begin
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	13
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	14	ML_file "Tools/Sledgehammer/async_manager.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	15	ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	16	ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	17	ML_file "Tools/Sledgehammer/sledgehammer_provers.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	18	ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	19	ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	20	ML_file "Tools/Sledgehammer/sledgehammer_mash.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	21	ML_file "Tools/Sledgehammer/sledgehammer_run.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	22	ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	23
42616 92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; wenzelm parents: 41094 diff changeset	24	setup {* Sledgehammer_Isar.setup *}
23444 6d4703843f93 added Metis setup (from Metis.thy); wenzelm parents: 21999 diff changeset	25
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	26	end

author	wenzelm
	Fri, 21 Sep 2012 17:28:53 +0200
changeset 49494	cbcccf2a0f6f
parent 48891	c0eafbd55de3
child 49881	d9d73ebf9274
permissions	-rw-r--r--