isabelle: File revisions

src/HOL/SAT.thy

2014-11-02	wenzelm	2014-11-02	modernized header uniformly as section;	file \| diff \| annotate
2014-02-01	wenzelm	2014-02-01	more standard file/module names;	file \| diff \| annotate
2012-10-31	blanchet	2012-10-31	moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong	file \| diff \| annotate
2012-10-31	blanchet	2012-10-31	moved Refute to "HOL/Library" to speed up building "Main" even more	file \| diff \| annotate
2012-08-22	wenzelm	2012-08-22	prefer ML_file over old uses;	file \| diff \| annotate
2012-01-03	blanchet	2012-01-03	tuned Refute	file \| diff \| annotate
2010-09-02	blanchet	2010-09-02	*use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd; this really* speeds up things -- HOL now builds 12% faster on my machine**	file \| diff \| annotate
2009-12-14	blanchet	2009-12-14	added "no_assms" option to Refute, and include structured proof assumptions by default; will do the same for Quickcheck unless there are objections	file \| diff \| annotate
2009-07-27	wenzelm	2009-07-27	proper context for SAT tactics; eliminated METAHYPS; tuned signatures;	file \| diff \| annotate
2009-03-16	wenzelm	2009-03-16	simplified method setup;	file \| diff \| annotate
2009-03-13	wenzelm	2009-03-13	unified type Proof.method and pervasive METHOD combinators;	file \| diff \| annotate
2008-04-02	haftmann	2008-04-02	tuned imports	file \| diff \| annotate
2006-11-29	wenzelm	2006-11-29	simplified method setup;	file \| diff \| annotate
2005-10-09	webertj	2005-10-09	Tactics sat and satx reimplemented, several improvements	file \| diff \| annotate
2005-09-29	wenzelm	2005-09-29	explicit dependencies of SAT vs. Refute; removed unused methods;	file \| diff \| annotate
2005-09-25	webertj	2005-09-25	sat_solver.ML not loaded anymore (already loaded by Refute.thy)	file \| diff \| annotate
2005-09-24	webertj	2005-09-24	cnf_struct renamed to cnf	file \| diff \| annotate
2005-09-24	obua	2005-09-24	preliminary fix of HOL build problem	file \| diff \| annotate
2005-09-23	webertj	2005-09-23	new sat tactic imports resolution proofs from zChaff	file \| diff \| annotate

isabelle

RSS Atom