content: {- |
  Module      :  ./CspCASLProver.hs
  Description :  Interface to the CspCASLProver (Isabelle based) theorem prover
  Copyright   :  (c) Liam O'Reilly and Markus Roggenbach, Swansea University 2009
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  csliam@swansea.ac.uk
  Stability   :  provisional
  Portability :  portable
  
  CspCASLProver allows interactive theorem proving on CspCASL
  specifications. See CspCASL.hs for details on the specification
  language CspCASL.
  
  "CspCASLProver.Consts" conatins constants and related fucntions for
  CspCASLProver.
  
  "CspCASLProver.CspCASLProver" is an interactive interface to the
  Isabelle prover (instanisated with CspProver). The encoding of CspCASL
  into IsabelleHOL requires the generation of several Isabelle theories
  where only the final theory requires user interaction.
  
  "CspCASLProver.CspProverConsts" contains Isabelle abstract syntax constants for
  CSP-Prover operations
  
  "CspCASLProver.IsabelleUtils" contains utilities for CspCASLProver
  related to Isabelle. The functions here typically manipulate Isabelle
  signatures.
  
  "CspCASLProver.TransProcesses" contains functions that implement CspCASLProver's
  translation of processes from CspCASL to CspProver.
  
  "CspCASLProver.Utils" contains utilities for CspCASLProver related to the actual
  construction of Isabelle theories.
  -}
  module CspCASLProver where
  