src/HOL/Tools/sat_funcs.ML
Mon, 10 Jul 2006 21:02:29 +0200 webertj minor optimization wrt. certifying terms
Fri, 07 Jul 2006 18:13:58 +0200 webertj "solver" reference added to make the SAT solver configurable
Mon, 03 Jul 2006 17:27:09 +0200 webertj comments fixed, minor optimization wrt. certifying terms
Wed, 03 May 2006 12:05:53 +0200 webertj pre_cnf_tac: beta-eta-normalization restricted to the current subgoal
Tue, 02 May 2006 19:23:48 +0200 webertj beta_eta_conversion added to pre_cnf_tac
Fri, 10 Mar 2006 16:31:50 +0100 webertj clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
Wed, 12 Oct 2005 18:17:48 +0200 webertj counter added to SAT signature
Wed, 12 Oct 2005 17:06:22 +0200 webertj no proof reconstruction when quick_and_dirty is set
Sun, 09 Oct 2005 17:06:03 +0200 webertj Tactics sat and satx reimplemented, several improvements
Wed, 28 Sep 2005 14:41:43 +0200 webertj pre_sat_tac moved towards end of file
Wed, 28 Sep 2005 14:16:12 +0200 webertj comment fixed
Sat, 24 Sep 2005 07:57:50 +0200 webertj replay_proof optimized: now performs backwards proof search
Sat, 24 Sep 2005 07:21:46 +0200 webertj code reformatted and restructured, many minor modifications
Fri, 23 Sep 2005 22:58:50 +0200 webertj new sat tactic imports resolution proofs from zChaff
less more (0) tip