isabelle: src/HOL/Sledgehammer.thy@d7b5fd465198 (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
41042 8275f52ac991 load "try" after "Metis" and move "Async_Manager" back to Sledgehammer blanchet parents: 40181 diff changeset	11	uses "Tools/Sledgehammer/async_manager.ML"
8275f52ac991 load "try" after "Metis" and move "Async_Manager" back to Sledgehammer blanchet parents: 40181 diff changeset	12	"Tools/Sledgehammer/sledgehammer_util.ML"
39947 f95834c8bb4d tuning blanchet parents: 39946 diff changeset	13	"Tools/Sledgehammer/sledgehammer_filter.ML"
40067 0783415ed7f0 renamed files blanchet parents: 39951 diff changeset	14	"Tools/Sledgehammer/sledgehammer_atp_translate.ML"
0783415ed7f0 renamed files blanchet parents: 39951 diff changeset	15	"Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML"
41087 d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems blanchet parents: 41042 diff changeset	16	"Tools/Sledgehammer/sledgehammer_provers.ML"
39947 f95834c8bb4d tuning blanchet parents: 39946 diff changeset	17	"Tools/Sledgehammer/sledgehammer_minimize.ML"
41087 d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems blanchet parents: 41042 diff changeset	18	"Tools/Sledgehammer/sledgehammer_run.ML"
39947 f95834c8bb4d tuning blanchet parents: 39946 diff changeset	19	"Tools/Sledgehammer/sledgehammer_isar.ML"
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	20	begin
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	21
39947 f95834c8bb4d tuning blanchet parents: 39946 diff changeset	22	setup {*
39951 ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: 39947 diff changeset	23	Sledgehammer.setup
39947 f95834c8bb4d tuning blanchet parents: 39946 diff changeset	24	#> Sledgehammer_Isar.setup
f95834c8bb4d tuning blanchet parents: 39946 diff changeset	25	*}
23444 6d4703843f93 added Metis setup (from Metis.thy); wenzelm parents: 21999 diff changeset	26
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	27	end

author	blanchet
	Wed, 08 Dec 2010 22:17:52 +0100
changeset 41087	d7b5fd465198
parent 41042	8275f52ac991
child 41094	1dc7652ce404
permissions	-rw-r--r--