# Theory Main

Up to index of Isabelle/HOL

theory Main
imports SAT Reconstruction
uses [Main.ML]
begin

    (*  Title:      HOL/Main.thy
        ID:         $Id: Main.thy,v 1.59 2005/09/29 13:50:44 wenzelm Exp $
    *)

    header {* Main HOL *}

    theory Main
    imports SAT Reconstruction
    begin

    text {*
      Theory @{text Main} includes everything.  Note that theory @{text
      PreList} already includes most HOL theories.
    *}

    text {* \medskip Late clause setup: installs \emph{all} simprules and
      claset rules into the clause cache; cf.\ theory @{text
      Reconstruction}. *}

    setup ResAxioms.clause_setup

    end