{- |
Module      :  $Id$
Description :  logic for the interactive higher order theorem prover Isabelle
Copyright   :  (c) Christian Maeder, DFKI Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable (except Isabelle.Logic_Isabelle)

This folder contains the interface to the Isabelle theorem prover.

"Isabelle.IsaSign" provides data structures for Isabelle signatures,
formulas and theories. These resemble the ML data structures that
Isabelle uses. However, the emphasis is on outputting theories
with the pretty printer ("Isabelle.IsaPrint"); hence, not only the
kernel language of Isabelle is supported. Because the Isabelle
logic is only used for proving, no parser and static analysis are provided.

"Isabelle.IsaProve" is an interactive interface to the Isabelle prover.
"Isabelle.CreateTheories" is the batch version.

"Isabelle.Logic_Isabelle" provides the Isabelle instance of
type class 'Logic.Logic.Logic'.

"Isabelle.IsaConsts" and
"Isabelle.Translate" are auxiliary modules used in the comorphisms
into Isabelle, as well as in the prover module.
-}

module Isabelle where