isabelle: File revisions

Mercurial Mercurial > repos > isabelle / file revisions

summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip

src/HOL/SAT.thy

2012-10-31	blanchet	moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong	file \| diff \| annotate
2012-10-31	blanchet	moved Refute to "HOL/Library" to speed up building "Main" even more	file \| diff \| annotate
2012-08-22	wenzelm	prefer ML_file over old uses;	file \| diff \| annotate
2012-01-03	blanchet	tuned Refute	file \| diff \| annotate
2010-09-02	blanchet	use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;	file \| diff \| annotate
2009-12-14	blanchet	added "no_assms" option to Refute, and include structured proof assumptions by default;	file \| diff \| annotate
2009-07-27	wenzelm	proper context for SAT tactics;	file \| diff \| annotate
2009-03-16	wenzelm	simplified method setup;	file \| diff \| annotate
2009-03-13	wenzelm	unified type Proof.method and pervasive METHOD combinators;	file \| diff \| annotate
2008-04-02	haftmann	tuned imports	file \| diff \| annotate
2006-11-29	wenzelm	simplified method setup;	file \| diff \| annotate
2005-10-09	webertj	Tactics sat and satx reimplemented, several improvements	file \| diff \| annotate
2005-09-29	wenzelm	explicit dependencies of SAT vs. Refute;	file \| diff \| annotate
2005-09-24	webertj	sat_solver.ML not loaded anymore (already loaded by Refute.thy)	file \| diff \| annotate
2005-09-24	webertj	cnf_struct renamed to cnf	file \| diff \| annotate
2005-09-24	obua	preliminary fix of HOL build problem	file \| diff \| annotate
2005-09-23	webertj	new sat tactic imports resolution proofs from zChaff	file \| diff \| annotate

less more (0) tip

isabelle