diff --git a/language-sally.cabal b/language-sally.cabal
--- a/language-sally.cabal
+++ b/language-sally.cabal
@@ -1,5 +1,5 @@
 name:                language-sally
-version:             0.1.0.0
+version:             0.1.0.1
 synopsis:            AST and pretty printer for Sally
 description:         AST and pretty printer for the Sally
                      <https://github.com/SRI-CSL/sally> input language
diff --git a/src/Language/Sally.hs b/src/Language/Sally.hs
--- a/src/Language/Sally.hs
+++ b/src/Language/Sally.hs
@@ -7,14 +7,31 @@
 -- Stability   :  experimental
 -- Portability :  unknown
 --
--- This module re-exports all the definitions from Language.Sally.*
+-- @language-sally@ is a package which contains a convenient AST and pretty
+-- printer for the input language of SRI's Sally model checker
+-- <https://github.com/SRI-CSL/sally>.
 --
+-- The main types exported by the package defined in "Language.Sally.Types"
+-- and correspond to the main block types in Sally's input language: the state
+-- type, state formula, transition formula, and transition system definition.
+--
+-- Low-level expressions and literals may be contructed using the functions in
+-- "Language.Sally.Expr", while the pretty printing mechanism is split between
+-- "Language.Sally.SExpPP" (dealing with layout of S-expressions) and
+-- "Language.Sally.PPrint" (dealing with the rendering of ASTs).
+--
+-- This module re-exports all the definitions from the submodules.
+--
 
 module Language.Sally (
-  module X
+    -- * re-exports
+    module Language.Sally.Expr
+  , module Language.Sally.PPrint
+  , module Language.Sally.SExpPP
+  , module Language.Sally.Types
 ) where
 
-import Language.Sally.Expr   as X
-import Language.Sally.PPrint as X
-import Language.Sally.SExpPP as X
-import Language.Sally.Types  as X
+import Language.Sally.Expr
+import Language.Sally.PPrint
+import Language.Sally.SExpPP
+import Language.Sally.Types
diff --git a/src/Language/Sally/Expr.hs b/src/Language/Sally/Expr.hs
--- a/src/Language/Sally/Expr.hs
+++ b/src/Language/Sally/Expr.hs
@@ -106,8 +106,8 @@
               else error "multExpr: non-linear arithmetic is not supported"
 
 -- | Determine if a Sally expression is a constant for the purposes of linear
--- multiplication. Note: this is an over approximation, e.g. (x + (-x))*y is a constant 0
--- times y, but will not pass this predicate.
+-- multiplication. Note: this is an over approximation, e.g. @(x + (-x))*y@
+-- is a constant equal to @0@ times @y@, but will not pass this predicate.
 isMultConst :: SallyExpr -> Bool
 isMultConst (SELit _) = True
 isMultConst (SEVar _) = False
@@ -121,19 +121,19 @@
 eqExpr :: SallyExpr -> SallyExpr -> SallyExpr
 eqExpr x y = SEPre (SPEq x y)
 
--- | @a `ltExpr` b@ represents the expression @a < b@.
+-- | @a \`ltExpr\` b@ represents the expression @a \< b@.
 ltExpr :: SallyExpr -> SallyExpr -> SallyExpr
 ltExpr x y = SEPre (SPLt x y)
 
--- | @a `leqExpr` b@ represents the expression @a <= b@.
+-- | @a \`leqExpr\` b@ represents the expression @a \<= b@.
 leqExpr :: SallyExpr -> SallyExpr -> SallyExpr
 leqExpr x y = SEPre (SPLEq x y)
 
--- | @a `gtExpr` b@ represents the expression @a > b@.
+-- | @a \`gtExpr\` b@ represents the expression @a > b@.
 gtExpr :: SallyExpr -> SallyExpr -> SallyExpr
 gtExpr x y = SEPre (SPGt x y)
 
--- | @a `geqExpr` b@ represents the expression @a >= b@.
+-- | @a \`geqExpr\` b@ represents the expression @a >= b@.
 geqExpr :: SallyExpr -> SallyExpr -> SallyExpr
 geqExpr x y = SEPre (SPGEq x y)
 
@@ -160,7 +160,7 @@
                                  ++ show x)
 
 -- | Create an if-then-else expression: @mux b x y@ represents the statement
--- "if b then x else y".
+-- @if b then x else y@.
 muxExpr :: SallyExpr -> SallyExpr -> SallyExpr -> SallyExpr
 muxExpr = SEMux
 
@@ -300,7 +300,7 @@
     _ -> a <| flattenOrs rest
 flattenOrs _ = undefined  -- make compiler happy :)
 
--- | Top-down rewriting of 'and' terms including constant folding and
+-- | Top-down rewriting of conjunctions of terms including constant folding and
 -- constructor reduction.
 simplifyAnds :: SallyPred -> SallyPred
 simplifyAnds p =
@@ -325,7 +325,7 @@
     SPGt    x y -> SPGt (constFold x) (constFold y)
     SPExpr  e   -> SPExpr (constFold e)
 
--- | Top-down rewriting of 'or' terms including constant folding and
+-- | Top-down rewriting of disjunctions including constant folding and
 -- constructor reduction.
 simplifyOrs :: SallyPred -> SallyPred
 simplifyOrs p =
diff --git a/src/Language/Sally/Types.hs b/src/Language/Sally/Types.hs
--- a/src/Language/Sally/Types.hs
+++ b/src/Language/Sally/Types.hs
@@ -180,10 +180,10 @@
                | SPImpl  SallyPred SallyPred     -- ^ implication
                | SPNot   SallyPred               -- ^ logical negation
                | SPEq    SallyExpr SallyExpr     -- ^ ==
-               | SPLEq   SallyExpr SallyExpr     -- ^ <=
-               | SPGEq   SallyExpr SallyExpr     -- ^ >=
-               | SPLt    SallyExpr SallyExpr     -- ^ <
-               | SPGt    SallyExpr SallyExpr     -- ^ >
+               | SPLEq   SallyExpr SallyExpr     -- ^ \<=
+               | SPGEq   SallyExpr SallyExpr     -- ^ \>=
+               | SPLt    SallyExpr SallyExpr     -- ^ \<
+               | SPGt    SallyExpr SallyExpr     -- ^ \>
   deriving (Show, Eq)
 
 instance ToSExp SallyPred where