isabelle: File revisions

src/HOL/ATP.thy

Tue, 09 Aug 2011 09:05:21 +0200	blanchet	load lambda-lifting structure earlier, so it can be used in Metis	file \| diff \| annotate
Tue, 05 Jul 2011 17:09:59 +0100	nik	improved translation of lambdas in THF	file \| diff \| annotate
Tue, 31 May 2011 16:38:36 +0200	blanchet	use "monomorph.ML" in "ATP" theory (so the new Metis can use it)	file \| diff \| annotate
Tue, 31 May 2011 16:38:36 +0200	blanchet	first step in sharing more code between ATP and Metis translation	file \| diff \| annotate
Tue, 26 Oct 2010 12:17:19 +0200	blanchet	reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers	file \| diff \| annotate
Mon, 25 Oct 2010 13:34:57 +0200	haftmann	moved sledgehammer to Plain; tuned dependencies	file \| diff \| annotate
Tue, 05 Oct 2010 12:50:45 +0200	blanchet	tuned comments	file \| diff \| annotate
Tue, 05 Oct 2010 11:10:37 +0200	blanchet	factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure	file \| diff \| annotate

isabelle