Proofs in development graphs. Follows Sect. IV:4.4 of the CASL Reference Manual. See also /Heterogeneous specification and the heterogeneous tool set/ (http://www.informatik.uni-bremen.de/~till/papers/habil.ps), section 5.6.

Proofs.Proofs contains data types for proofs

Proofs.EdgeUtils and Proofs.StatusUtils contain utilities.

The proof calculus for development graphs is contained in the following modules:

Proofs.InferBasic rule basic inference

Proofs.Global rules global decomposition, global subsumption

Proofs.Local rules local decomposition, local subsumption (these are derived rules in the calculus)

Proofs.Composition various composition rules

Proofs.HideTheoremShift rule Hide-Theorem-Shift

Proofs.TheoremHideShift rule Theorem-Hide-Shift

The remaining rules have not been implemented yet.