Isabelle/Weidenbach_Book sessions

CDCL

This session the CDCL calculi (Weidenbach and Nieuwenhuis et al.) and the links between
  both. It also contains a very simple implementation based on lists and two extensions (restart and
  incremental).

  This version is based on the Refinement Framework, to make the two-watched-literals part easier to compile
  (workaround as long as a session cannot have two parents).
CDCL_Extensions

This sessions contains the extensions of the CDCL calculus.
Entailment_Definition

This session contains various (but still general) definition of entailment used
  later.
IsaSAT

We here refine the previous session to generate code.
Normalisation

This session contains the normalisation from general formulas to CNF and DNF.
Weidenbach_Book_Base

This session imports HOL, some additional useful theories from HOL, and our own
  extensions above these lemmas.