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.