Theorem Prover Written in Haskell

Term.lhs Defines the type of propositional expressions (terms)
Theorem.lhs Defines the type of theorems and primitive inference rules
Inferences.lhs Examples of adding your own inference rules
InfLib.lhs Some inference rules the next two modules need
Tactical.lhs Goal-directed backward inferences, aka tactics
MonadicTactical Goal-directed backward inferences are monads!