{- |
Proofs in development graphs.
Follows Sect. IV:4.4 of the CASL Reference Manual.
See also /Heterogeneous
specification and the heterogeneous tool set/
(), 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.
-}
module Proofs where