isabelle: src/HOL/ATP.thy@a88d6073b190 (annotated)

39951 ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	1	(* Title: HOL/ATP.thy
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	2	Author: Fabian Immler, TU Muenchen
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	3	Author: Jasmin Blanchette, TU Muenchen
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	4	*)
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	5
39958 88c9aa5666de tuned comments blanchet parents: 39951 diff changeset	6	header {* Automatic Theorem Provers (ATPs) *}
39951 ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	7
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	8	theory ATP
40121 e7a80c6752c9 moved sledgehammer to Plain; tuned dependencies haftmann parents: 39958 diff changeset	9	imports HOL
e7a80c6752c9 moved sledgehammer to Plain; tuned dependencies haftmann parents: 39958 diff changeset	10	uses
e7a80c6752c9 moved sledgehammer to Plain; tuned dependencies haftmann parents: 39958 diff changeset	11	"Tools/ATP/atp_problem.ML"
e7a80c6752c9 moved sledgehammer to Plain; tuned dependencies haftmann parents: 39958 diff changeset	12	"Tools/ATP/atp_proof.ML"
e7a80c6752c9 moved sledgehammer to Plain; tuned dependencies haftmann parents: 39958 diff changeset	13	"Tools/ATP/atp_systems.ML"
39951 ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	14	begin
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	15
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	16	setup ATP_Systems.setup
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	17
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	18	end

author	blanchet
	Tue, 26 Oct 2010 11:11:23 +0200
changeset 40158	a88d6073b190
parent 40121	e7a80c6752c9
child 40178	00152d17855b
permissions	-rw-r--r--