content: {- |
  Description :  Proofs in development graphs
  Copyright   :  (c) Otto-von-Guericke University of Magdeburg
  License     :  GPLv2 or higher, see LICENSE.txt
  
  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.
  -}
  
  module Proofs where
  