diff --git a/copilot-libraries.cabal b/copilot-libraries.cabal
--- a/copilot-libraries.cabal
+++ b/copilot-libraries.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-libraries
-version:             0.3
+version:             0.4
 synopsis:            A Haskell-embedded DSL for monitoring hard real-time
                      distributed systems.
 description:         
@@ -42,6 +42,7 @@
     mtl >= 2.0
 
   exposed-modules:
+    Copilot.Library.Libraries
     Copilot.Library.Clocks
     Copilot.Library.LTL
     Copilot.Library.PTLTL
@@ -50,8 +51,6 @@
     Copilot.Library.Utils
     Copilot.Library.Voting
     Copilot.Library.Stacks
-
-  other-modules:
 
   ghc-options:
     -fwarn-tabs
diff --git a/src/Copilot/Library/Clocks.hs b/src/Copilot/Library/Clocks.hs
--- a/src/Copilot/Library/Clocks.hs
+++ b/src/Copilot/Library/Clocks.hs
@@ -1,3 +1,7 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
 -- | A library that generates new clocks based on a base period.
 -- Usage, supposing @v@ is a Copilot variable, then
 -- @
@@ -17,7 +21,6 @@
 -- The period must be greater than 0.
 -- The phase must be greater than or equal to 0.
 -- The phase must be less than the period.
-
 
 module Copilot.Library.Clocks
   ( clk, clk1, period, phase ) where
diff --git a/src/Copilot/Library/LTL.hs b/src/Copilot/Library/LTL.hs
--- a/src/Copilot/Library/LTL.hs
+++ b/src/Copilot/Library/LTL.hs
@@ -1,3 +1,7 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
 -- | Bounded Linear Temporal Logic (LTL) operators.  For a bound @n@, a property
 -- @p@ holds if it holds on the next @n@ transitions (between periods).  If
 -- @n == 0@, then the trace includes only the current period.  For example,
diff --git a/src/Copilot/Library/Libraries.hs b/src/Copilot/Library/Libraries.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Library/Libraries.hs
@@ -0,0 +1,26 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | Main import module for the front-end lanugage.
+
+module Copilot.Library.Libraries (
+    module Copilot.Library.Clocks
+  , module Copilot.Library.LTL
+  , module Copilot.Library.PTLTL
+  , module Copilot.Library.Statistics
+  , module Copilot.Library.RegExp
+  , module Copilot.Library.Utils
+  , module Copilot.Library.Voting
+  , module Copilot.Library.Stacks
+  ) where
+
+import Copilot.Library.Clocks
+import Copilot.Library.LTL
+import Copilot.Library.PTLTL
+import Copilot.Library.Statistics
+import Copilot.Library.RegExp
+import Copilot.Library.Utils
+import Copilot.Library.Voting
+import Copilot.Library.Stacks
+
diff --git a/src/Copilot/Library/PTLTL.hs b/src/Copilot/Library/PTLTL.hs
--- a/src/Copilot/Library/PTLTL.hs
+++ b/src/Copilot/Library/PTLTL.hs
@@ -1,3 +1,7 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
 -- | Provides past-time linear-temporal logic (ptLTL operators).
 --
 -- Interface: see Examples/PTLTLExamples.hs.
diff --git a/src/Copilot/Library/RegExp.hs b/src/Copilot/Library/RegExp.hs
--- a/src/Copilot/Library/RegExp.hs
+++ b/src/Copilot/Library/RegExp.hs
@@ -1,5 +1,6 @@
 module Copilot.Library.RegExp ( copilotRegexp, copilotRegexpB ) where
 
+-- | A regular expression librariy.
 
 import Text.ParserCombinators.Parsec
   ( optional, (<|>), string, char, between, GenParser, many, choice, CharParser
diff --git a/src/Copilot/Library/Stacks.hs b/src/Copilot/Library/Stacks.hs
--- a/src/Copilot/Library/Stacks.hs
+++ b/src/Copilot/Library/Stacks.hs
@@ -1,12 +1,16 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | Stack machine.
+
 {-# LANGUAGE NoImplicitPrelude #-}
 
 module Copilot.Library.Stacks
   ( stack, stack' ) where
 
-
 import Copilot.Language
 import Copilot.Language.Prelude
-
 
 type PushSignal    = Stream Bool
 type PopSignal     = Stream Bool
diff --git a/src/Copilot/Library/Statistics.hs b/src/Copilot/Library/Statistics.hs
--- a/src/Copilot/Library/Statistics.hs
+++ b/src/Copilot/Library/Statistics.hs
@@ -1,3 +1,7 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
 -- | Basic bounded statistics.  In the following, a bound @n@ is given stating
 -- the number of periods over which to compute the statistic (@n == 1@ computes
 -- it only over the current period).
diff --git a/src/Copilot/Library/Utils.hs b/src/Copilot/Library/Utils.hs
--- a/src/Copilot/Library/Utils.hs
+++ b/src/Copilot/Library/Utils.hs
@@ -1,14 +1,18 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | Utility bounded-list functions (e.g., folds, scans, etc.)
+
 module Copilot.Library.Utils
     ( take, tails, nfoldl, nfoldl1, nfoldr, nfoldr1,
       nscanl, nscanr, nscanl1, nscanr1,
       case', (!!), cycle ) 
 where
 
-
 import Copilot.Language
 import Copilot.Language.Prelude 
 import qualified Prelude as P
-
 
 -- | functions similar to the Prelude functions on lists