{- |

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