diff --git a/Setup.hs b/Setup.hs
--- a/Setup.hs
+++ b/Setup.hs
@@ -1,2 +1,93 @@
 import Distribution.Simple
 main = defaultMain
+
+{- Inferring the package version from git. Posted by https://github.com/hvr
+ -
+ - https://gist.github.com/656738
+
+import Control.Exception
+import Control.Monad
+import Data.Maybe
+import Data.Version
+import Distribution.PackageDescription (PackageDescription(..), HookedBuildInfo, GenericPackageDescription(..))
+import Distribution.Package (PackageIdentifier(..))
+import Distribution.Simple (defaultMainWithHooks, simpleUserHooks, UserHooks(..))
+import Distribution.Simple.LocalBuildInfo (LocalBuildInfo(..))
+import Distribution.Simple.Setup (BuildFlags(..), ConfigFlags(..))
+import Distribution.Simple.Utils (die)
+import System.Process (readProcess)
+import Text.ParserCombinators.ReadP (readP_to_S)
+
+main :: IO ()
+main = defaultMainWithHooks simpleUserHooks
+         { confHook = myConfHook
+         , buildHook = myBuildHook
+         }
+
+-- configure hook
+myConfHook :: (GenericPackageDescription, HookedBuildInfo)
+           -> ConfigFlags
+           -> IO LocalBuildInfo
+myConfHook (gpdesc, hbinfo) cfg = do
+  let GenericPackageDescription {
+        packageDescription = pdesc@PackageDescription {
+           package = pkgIden }} = gpdesc
+
+  gitVersion <- inferVersionFromGit (pkgVersion (package pdesc))
+
+  let gpdesc' = gpdesc {
+        packageDescription = pdesc {
+           package = pkgIden { pkgVersion = gitVersion } } }
+
+  -- putStrLn $ showVersion gitVersion
+
+  confHook simpleUserHooks (gpdesc', hbinfo) cfg
+
+
+-- build hook
+myBuildHook :: PackageDescription
+            -> LocalBuildInfo
+            -> UserHooks
+            -> BuildFlags
+            -> IO ()
+myBuildHook pdesc lbinfo uhooks bflags = do
+  let lastVersion = pkgVersion $ package pdesc
+
+  gitVersion <- inferVersionFromGit lastVersion 
+
+  when (gitVersion /= lastVersion) $
+    die("The version reported by git '" ++ showVersion gitVersion ++
+        "' has changed since last time this package was configured (version was '" ++
+        showVersion lastVersion ++ "' back then), please re-configure package")
+
+  buildHook simpleUserHooks pdesc lbinfo uhooks bflags
+
+-- |Infer package version from Git tags. Uses `git describe` to infer 'Version'.
+inferVersionFromGit :: Version -> IO Version
+inferVersionFromGit version0 = do
+  ver_line <- init `liftM` readProcess "git"
+              [ "describe"
+              , "--abbrev=5"
+              , "--tags"
+              , "--match=v[0-9].[0-9][0-9]"
+              , "--dirty"
+              , "--long"
+              , "--always"
+              ] ""
+
+  -- ver_line <- return "v0.1-42-gf9f4eb3-dirty"
+  putStrLn ver_line
+  -- let versionStr = ver_line -- (head ver_line == 'v') `assert` replaceFirst '-' '.' (tail ver_line)
+      -- Just version = listToMaybe [ p | (p, "") <- readP_to_S parseVersion versionStr ]
+
+  return version0
+
+{-
+-- | Helper for replacing first occurence of character by another one.
+replaceFirst :: Eq a => a -> a -> [a] -> [a]
+replaceFirst _ _ [] = []
+replaceFirst o r (x:xs) | o == x    = r : xs
+                        | otherwise = x : replaceFirst o r xs
+-}
+
+-}
diff --git a/src/Control/Monad/Bind.hs b/src/Control/Monad/Bind.hs
--- a/src/Control/Monad/Bind.hs
+++ b/src/Control/Monad/Bind.hs
@@ -45,6 +45,8 @@
 import Control.Monad.State
 import Control.Monad.Fresh
 
+import qualified Control.Monad.Trans.PreciseFresh as Precise
+
 ------------------------------------------------------------------------------
 -- Bindings
 ------------------------------------------------------------------------------
@@ -64,6 +66,9 @@
 
 instance Monad m => MonadBind k v (StateT (Bindings k v) m) where
 
+instance MonadBind k v m => MonadBind k v (FreshT m) where
+instance MonadBind k v m => MonadBind k v (Precise.FreshT m) where
+
 ------------------------------------------------------------------------------
 -- Type synonym for the StateT monad transformer
 ------------------------------------------------------------------------------
@@ -121,8 +126,9 @@
 -- | @importBinding mkR d n@ checks if there is already a binding registered
 -- for the value @d@ and if not it generates a fresh identifier using the name
 -- @n@ as a hint and converting name and identifier to a value using $mkR$.
+{-# INLINE importBinding #-}
 importBinding :: (MonadBind k v m, MonadFresh m, Show v, Show k, Ord k) 
-               => (String -> Int -> v) 
+               => (String -> Integer -> v) 
                -> k 
                -> String -> m v
 importBinding mkR k n = do
diff --git a/src/Control/Monad/Fresh.hs b/src/Control/Monad/Fresh.hs
--- a/src/Control/Monad/Fresh.hs
+++ b/src/Control/Monad/Fresh.hs
@@ -18,7 +18,7 @@
   , evalFresh
   , execFresh
 
-  -- * The FreshT monad transformer
+  -- * The fast FreshT monad transformer
   , FreshT(..)
   , freshT
   , runFreshT
@@ -40,5 +40,5 @@
 import Control.Monad.Trans
 
 import Control.Monad.Fresh.Class
-import Control.Monad.Trans.Fresh hiding (freshIdent)
+import Control.Monad.Trans.FastFresh hiding (freshIdents)
 
diff --git a/src/Control/Monad/Fresh/Class.hs b/src/Control/Monad/Fresh/Class.hs
--- a/src/Control/Monad/Fresh/Class.hs
+++ b/src/Control/Monad/Fresh/Class.hs
@@ -18,31 +18,47 @@
 import Control.Monad.Reader
 import Control.Monad.Writer
 
-import qualified Control.Monad.Trans.Fresh as Fresh (FreshT, freshIdent)
+import qualified Control.Monad.Trans.FastFresh    as Fast (FreshT, freshIdents)
+import qualified Control.Monad.Trans.PreciseFresh as Precise (FreshT, freshIdent, freshIdents)
 
 -- Added 'Applicative' until base states this hierarchy
 class (Applicative m, Monad m) => MonadFresh m where
-    freshIdent :: String -- ^ Desired name.
-               -> m Int  -- ^ Fresh identifier.
+    -- | Get the integer of the next fresh identifier of this name.
+    freshIdent  :: String   -- ^ Desired name
+                -> m Integer
 
+    -- | Get a number of fresh identifiers. This reserves the required number
+    -- of identifiers on all names.
+    freshIdents :: Integer    -- ^ Number of desired fresh identifiers.
+                -> m Integer  -- ^ The first Fresh identifier.
 
-instance (Functor m, Monad m) => MonadFresh (Fresh.FreshT m) where
-    freshIdent = Fresh.freshIdent
 
+instance (Functor m, Monad m) => MonadFresh (Fast.FreshT m) where
+    freshIdent _name = Fast.freshIdents 1
+    freshIdents      = Fast.freshIdents
 
+instance (Functor m, Monad m) => MonadFresh (Precise.FreshT m) where
+    freshIdent  = Precise.freshIdent
+    freshIdents = Precise.freshIdents
+
+
 ----------------------------------------------------------------------------
 -- instances for other mtl transformers
 --
 -- TODO: Add remaining ones
 
 instance MonadFresh m => MonadFresh (MaybeT m) where
-    freshIdent = lift . freshIdent
+    freshIdent  = lift . freshIdent
+    freshIdents = lift . freshIdents
 
 instance MonadFresh m => MonadFresh (StateT s m) where
-    freshIdent = lift . freshIdent
+    freshIdent  = lift . freshIdent
+    freshIdents = lift . freshIdents
 
 instance MonadFresh m => MonadFresh (ReaderT r m) where
-    freshIdent = lift . freshIdent
+    freshIdent  = lift . freshIdent
+    freshIdents = lift . freshIdents
 
 instance (Monoid w, MonadFresh m) => MonadFresh (WriterT w m) where
-    freshIdent = lift . freshIdent
+    freshIdent  = lift . freshIdent
+    freshIdents = lift . freshIdents
diff --git a/src/Control/Monad/Trans/FastFresh.hs b/src/Control/Monad/Trans/FastFresh.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Trans/FastFresh.hs
@@ -0,0 +1,114 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}  -- require for MonadError
+-- |
+-- Copyright   : (c) 2010 Simon Meier
+-- License     : GPL v3 (see LICENSE)
+-- 
+-- Maintainer  : Simon Meier <iridcode@gmail.com>
+-- Portability : GHC only
+--
+-- A monad transformer for passing a fast fresh name supply through a
+-- computation. It uses an 'Integer' counter to determine the next free name.
+--
+-- Modeled after the mtl-2.0 library.
+--
+module Control.Monad.Trans.FastFresh (
+
+  -- * The Fresh monad
+    Fresh
+  , runFresh
+  , evalFresh
+  , execFresh
+
+  -- * The FreshT monad transformer
+  , FreshT(..)
+  , freshT
+  , runFreshT
+  , evalFreshT
+  , execFreshT
+
+  -- * Fresh name generation
+  , FreshState
+  , nothingUsed
+  , freshIdents
+
+  ) where
+
+import Control.Basics
+import Control.Monad.Identity
+import Control.Monad.State.Strict
+import Control.Monad.Error
+import Control.Monad.Reader
+
+------------------------------------------------------------------------------
+-- FreshT monad transformer
+------------------------------------------------------------------------------
+
+-- | The state of the name supply: the first unused sequence number of every name.
+type FreshState = Integer
+
+-- | A computation that can generate fresh variables from name hints.
+newtype FreshT m a = FreshT { unFreshT :: StateT FreshState m a }
+    deriving( Functor, Applicative, Alternative, Monad, MonadPlus, MonadTrans )
+
+-- | Construct a 'FreshT' action from a 'FreshState' modification.
+freshT :: (FreshState -> m (a, FreshState)) -> FreshT m a
+freshT = FreshT . StateT
+
+-- | The empty fresh state.
+nothingUsed :: FreshState
+nothingUsed = 0
+
+-- | Run a computation with a fresh name supply.
+runFreshT :: FreshT m a -> FreshState -> m (a, FreshState)
+runFreshT (FreshT m) used = runStateT m used
+
+-- | Evaluate a computation with a fresh name supply.
+evalFreshT :: Monad m => FreshT m a -> FreshState -> m a
+evalFreshT (FreshT m) used = evalStateT m used
+
+-- | Execute a computation with a fresh name supply.
+execFreshT :: Monad m => FreshT m a -> FreshState -> m FreshState
+execFreshT (FreshT m) used = execStateT m used
+
+-- | Get 'k' fresh identifiers.
+freshIdents :: Monad m
+            => Integer           -- ^ number of desired identifiers
+            -> FreshT m Integer  -- ^ The first fresh identifier.
+freshIdents k = do
+    i <- FreshT get
+    FreshT $ put $ i + k
+    return i
+
+-- Instances
+------------
+
+instance MonadError e m => MonadError e (FreshT m) where
+    throwError     = lift . throwError
+    catchError m h = FreshT $ catchError (unFreshT m) (unFreshT . h)
+
+instance MonadReader r m => MonadReader r (FreshT m) where
+    ask       = lift ask
+    local f m = FreshT $ local f $ unFreshT m
+
+instance MonadState s m => MonadState s (FreshT m) where
+    get   = lift get
+    put s = lift $ put s
+
+------------------------------------------------------------------------------
+-- Fresh monad
+------------------------------------------------------------------------------
+
+type Fresh = FreshT Identity
+
+-- | Run a computation with a fresh name supply.
+runFresh :: Fresh a -> FreshState -> (a, FreshState)
+runFresh (FreshT m) used = runState m used
+
+-- | Evaluate a computation with a fresh name supply.
+evalFresh :: Fresh a -> FreshState -> a
+evalFresh (FreshT m) used = evalState m used
+
+-- | Execute a computation with a fresh name supply.
+execFresh :: Fresh a -> FreshState -> FreshState
+execFresh (FreshT m) used = execState m used
diff --git a/src/Control/Monad/Trans/Fresh.hs b/src/Control/Monad/Trans/Fresh.hs
deleted file mode 100644
--- a/src/Control/Monad/Trans/Fresh.hs
+++ /dev/null
@@ -1,110 +0,0 @@
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}  -- require for MonadError
--- |
--- Copyright   : (c) 2010 Simon Meier
--- License     : GPL v3 (see LICENSE)
--- 
--- Maintainer  : Simon Meier <iridcode@gmail.com>
--- Portability : GHC only
---
--- A monad transformer for passing a fresh name supply through a computation.
--- This is just a newtype wrapper around the 'StateT' monad transformer.
---
--- Modeled after the mtl-2.0 library.
---
-module Control.Monad.Trans.Fresh (
-
-  -- * The Fresh monad
-    Fresh
-  , runFresh
-  , evalFresh
-  , execFresh
-
-  -- * The FreshT monad transformer
-  , FreshT(..)
-  , freshT
-  , runFreshT
-  , evalFreshT
-  , execFreshT
-
-  -- * Fresh name generation
-  , FreshState
-  , nothingUsed
-  , freshIdent
-
-  ) where
-
-import Control.Basics
-import Control.Monad.Identity
-import Control.Monad.State.Strict
-import Control.Monad.Error
-import Control.Monad.Reader
-
-------------------------------------------------------------------------------
--- FreshT monad transformer
-------------------------------------------------------------------------------
-
--- | The state of the name supply: the last used sequence number of every name.
-type FreshState = Int
-
--- | A computation that can generate fresh variables from name hints.
-newtype FreshT m a = FreshT { unFreshT :: StateT FreshState m a }
-    deriving( Functor, Applicative, Alternative, Monad, MonadPlus, MonadTrans )
-
--- | Construct a 'FreshT' action from a 'FreshState' modification.
-freshT :: (FreshState -> m (a, FreshState)) -> FreshT m a
-freshT = FreshT . StateT
-
--- | The empty fresh state.
-nothingUsed :: FreshState
-nothingUsed = 0
-
--- | Run a computation with a fresh name supply.
-runFreshT :: FreshT m a -> FreshState -> m (a, FreshState)
-runFreshT (FreshT m) used = runStateT m used
-
--- | Evaluate a computation with a fresh name supply.
-evalFreshT :: Monad m => FreshT m a -> FreshState -> m a
-evalFreshT (FreshT m) used = evalStateT m used
-
--- | Execute a computation with a fresh name supply.
-execFreshT :: Monad m => FreshT m a -> FreshState -> m FreshState
-execFreshT (FreshT m) used = execStateT m used
-
--- | Get a fresh identifier.
-freshIdent :: Monad m 
-           => String        -- ^ Desired name.
-           -> FreshT m Int  -- ^ Fresh identifier for this name.
-freshIdent _ = do
-    i <- FreshT get
-    FreshT $ put $ succ i
-    return i
-
--- Instances
-------------
-
-instance MonadError e m => MonadError e (FreshT m) where
-    throwError     = lift . throwError
-    catchError m h = FreshT $ catchError (unFreshT m) (unFreshT . h)
-
-instance MonadReader r m => MonadReader r (FreshT m) where
-    ask       = lift ask
-    local f m = FreshT $ local f $ unFreshT m
-
-------------------------------------------------------------------------------
--- Fresh monad
-------------------------------------------------------------------------------
-
-type Fresh = FreshT Identity
-
--- | Run a computation with a fresh name supply.
-runFresh :: Fresh a -> FreshState -> (a, FreshState)
-runFresh (FreshT m) used = runState m used
-
--- | Evaluate a computation with a fresh name supply.
-evalFresh :: Fresh a -> FreshState -> a
-evalFresh (FreshT m) used = evalState m used
-
--- | Execute a computation with a fresh name supply.
-execFresh :: Fresh a -> FreshState -> FreshState
-execFresh (FreshT m) used = execState m used
diff --git a/src/Control/Monad/Trans/PreciseFresh.hs b/src/Control/Monad/Trans/PreciseFresh.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Trans/PreciseFresh.hs
@@ -0,0 +1,129 @@
+{-# LANGUAGE BangPatterns, GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}  -- require for MonadError
+-- |
+-- Copyright   : (c) 2010-2012 Simon Meier
+-- License     : GPL v3 (see LICENSE)
+-- 
+-- Maintainer  : Simon Meier <iridcode@gmail.com>
+-- Portability : GHC only
+--
+-- A monad transformer for passing a fresh name supply through a computation.
+-- The name supply is precise in the sense that every 'String' has its own
+-- supply of indices for the next fresh name.
+--
+-- Modeled after the mtl-2.0 library.
+--
+module Control.Monad.Trans.PreciseFresh (
+
+  -- * The Fresh monad
+    Fresh
+  , runFresh
+  , evalFresh
+  , execFresh
+
+  -- * The FreshT monad transformer
+  , FreshT(..)
+  , freshT
+  , runFreshT
+  , evalFreshT
+  , execFreshT
+
+  -- * Fresh name generation
+  , FreshState
+  , nothingUsed
+  , freshIdent
+  , freshIdents
+
+  ) where
+
+import Control.Basics
+import Control.Monad.Identity
+import Control.Monad.State.Strict
+import Control.Monad.Error
+import Control.Monad.Reader
+
+import qualified Data.Map as M
+
+------------------------------------------------------------------------------
+-- FreshT monad transformer
+------------------------------------------------------------------------------
+
+-- | The state of the name supply: the first unused sequence number of every name.
+type FreshState = M.Map String Integer
+
+-- | A computation that can generate fresh variables from name hints.
+newtype FreshT m a = FreshT { unFreshT :: StateT FreshState m a }
+    deriving( Functor, Applicative, Alternative, Monad, MonadPlus, MonadTrans )
+
+-- | Construct a 'FreshT' action from a 'FreshState' modification.
+freshT :: (FreshState -> m (a, FreshState)) -> FreshT m a
+freshT = FreshT . StateT
+
+-- | The empty fresh state.
+nothingUsed :: FreshState
+nothingUsed = M.empty
+
+-- | Run a computation with a fresh name supply.
+runFreshT :: FreshT m a -> FreshState -> m (a, FreshState)
+runFreshT (FreshT m) used = runStateT m used
+evalFreshT :: Monad m => FreshT m a -> FreshState -> m a
+evalFreshT (FreshT m) used = evalStateT m used
+
+-- | Execute a computation with a fresh name supply.
+execFreshT :: Monad m => FreshT m a -> FreshState -> m FreshState
+execFreshT (FreshT m) used = execStateT m used
+
+-- | /O(log(n))/. Get a fresh identifier for the given name.
+freshIdent :: Monad m => String -> FreshT m Integer
+freshIdent name = do
+    m <- FreshT get
+    let i  = M.findWithDefault 0 name m
+        !i' = succ i -- avoid building thunks in the Map
+    FreshT (modify (M.insert name i'))
+    return i
+
+-- | /O(n)/. Get 'k' fresh identifiers.
+freshIdents :: Monad m
+            => Integer           -- ^ number of desired identifiers
+            -> FreshT m Integer  -- ^ The first fresh identifier.
+freshIdents k = do
+    m <- FreshT get
+    let maxIdx = maximum $ 0 : map snd (M.toList m)
+        nextIdx = maxIdx + k
+    -- insert 'nextIdx' at "" to remember it for the next call
+    FreshT (put (M.insert "" nextIdx $ M.map (const nextIdx) m))
+    return maxIdx
+
+
+-- Instances
+------------
+
+instance MonadError e m => MonadError e (FreshT m) where
+    throwError     = lift . throwError
+    catchError m h = FreshT $ catchError (unFreshT m) (unFreshT . h)
+
+instance MonadReader r m => MonadReader r (FreshT m) where
+    ask       = lift ask
+    local f m = FreshT $ local f $ unFreshT m
+
+instance MonadState s m => MonadState s (FreshT m) where
+    get   = lift get
+    put s = lift $ put s
+
+------------------------------------------------------------------------------
+-- Fresh monad
+------------------------------------------------------------------------------
+
+type Fresh = FreshT Identity
+
+-- | Run a computation with a fresh name supply.
+runFresh :: Fresh a -> FreshState -> (a, FreshState)
+runFresh (FreshT m) used = runState m used
+
+-- | Evaluate a computation with a fresh name supply.
+evalFresh :: Fresh a -> FreshState -> a
+evalFresh (FreshT m) used = evalState m used
+
+-- | Execute a computation with a fresh name supply.
+execFresh :: Fresh a -> FreshState -> FreshState
+execFresh (FreshT m) used = execState m used
diff --git a/src/Data/DAG/Simple.hs b/src/Data/DAG/Simple.hs
--- a/src/Data/DAG/Simple.hs
+++ b/src/Data/DAG/Simple.hs
@@ -1,23 +1,36 @@
 -- |
--- Copyright   : (c) 2010 Simon Meier
+-- Copyright   : (c) 2010,2012 Simon Meier
 -- License     : GPL v3 (see LICENSE)
 -- 
 -- Maintainer  : Simon Meier <iridcode@gmail.com>
 --
 -- Simple  vertice list based representation of DAGs and some common operations on it.
 module Data.DAG.Simple (
-    toposort
+  -- * Computing with binary relations
+    Relation
+  , inverse
+  , image
   , reachableSet
+  , restrict
+
+  -- ** Cycles
+  , dfsLoopBreakers
   , cyclic
+  , toposort
+
 ) where
 
 
-import Data.List
-import qualified Data.Set as S
+import           Control.Basics
+import           Control.Monad.Writer
+import           Control.Monad.RWS
 
-import Control.Basics
-import Control.Monad.Writer
+import           Data.List
+import qualified Data.DList as D
+import qualified Data.Set   as S
 
+-- import Test.QuickCheck.Property (label)
+-- import Test.QuickCheck (quickCheck)
 
 -- | Produce a topological sorting of the given relation. If the relation is
 -- cyclic, then the result is at least some permutation of all elements of
@@ -31,7 +44,7 @@
       | otherwise            =
           foldM visit (S.insert x visited) preds <* tell (pure x)
       where
-        preds = [ e | (e,e') <- dag, e' == x ]
+        preds = x `image` inverse dag
 
 
 -- | Compute the set of nodes reachable from the given set of nodes.
@@ -42,9 +55,7 @@
     visit visited x 
       | x `S.member` visited = visited
       | otherwise            =
-          foldl' visit (S.insert x visited) succs
-      where
-        succs = [ e' | (e,e') <- dag, e == x ]
+          foldl' visit (S.insert x visited) (x `image` dag)
 
 -- | Is the relation cyclic.
 cyclic :: Ord a => [(a,a)] -> Bool
@@ -64,3 +75,66 @@
         next     = [ e' | (e,e') <- rel, e == x ]
         parents' = S.insert x parents
 
+
+-- TODO: Consider implementing something along the lines of Ann Becker, Dan
+-- Geiger, Optimization of Pearl's method of conditioning and greedy-like
+-- approximation algorithms for the vertex feedback set problem, Artificial
+-- Intelligence, Volume 83, Issue 1, May 1996, Pages 167-188, ISSN 0004-3702,
+-- 10.1016/0004-3702(95)00004-6.
+-- <http://www.sciencedirect.com/science/article/pii/0004370295000046>.
+
+-- | Compute a minimal set of loop-breakers using a greedy DFS strategy. A set
+-- of loop-breakers is a set of nodes such that removing them ensures the
+-- acyclicity of the relation. It is minimal, if no node can be removed from
+-- the set.
+dfsLoopBreakers :: Ord a => [(a,a)] -> [a]
+dfsLoopBreakers rel = 
+    D.toList $ snd $ execRWS (mapM_ (visit . fst) rel) () S.empty
+  where 
+    visit x = do
+        visited <- gets (S.member x)
+        unless visited $ findLoopBreakers S.empty x
+
+    -- PRE: x0 is not yet visited
+    findLoopBreakers parents0 x = do
+        modify (S.insert x)
+        let parents = S.insert x parents0
+            ys      = x `image` rel
+        if any (`S.member` parents) ys
+          then tell (return x) 
+          else forM_ ys $ \y -> do 
+                   visited <- gets (S.member y)
+                   unless visited $ findLoopBreakers parents y
+
+-- | A relation represented as a list of tuples.
+type Relation a = [(a,a)]
+
+-- | Restrict a relation to elements satisfying a predicate.
+restrict :: Eq a => (a -> Bool) -> Relation a -> Relation a
+restrict p = filter (\(x,y) -> p x && p y)
+
+-- | The image of an element under a 'Relation'.
+image :: Eq a => a -> Relation a -> [a]
+image x rel = [ y' | (x', y') <- rel, x == x' ]
+
+-- | The inverse of a 'Relation'.
+inverse :: Relation a -> Relation a
+inverse rel = [ (y,x) | (x, y) <- rel ]
+
+{-
+prop_dfsLoopBreakers noSelfLoops rel0
+  | cyclic rel = label cycleLabel (minimal && not (cyclic (rel' breakers)))
+  | otherwise  = label "acyclic" (null breakers)
+  where
+    -- remove (x,x) entries in half of the cases
+    removeSelfLoops | noSelfLoops = filter (not . (uncurry (==)))
+                    | otherwise   = id
+    -- restrict the relation to get more cyclic cases
+    rel      =  removeSelfLoops $ map ((`mod` (20 :: Int)) *** (`mod` 20)) rel0
+    rel' bs  = restrict (not . (`elem` bs)) rel
+    breakers = dfsLoopBreakers rel
+    cycleLabel | any (uncurry (==)) rel = "cyclic (with self-loop)"
+               | otherwise              = "cyclic (no self-loop)"
+    -- true if loop breakers are minimal
+    minimal = all (\b -> cyclic (rel' (filter (/= b) breakers))) breakers
+-}
diff --git a/src/Extension/Data/Bounded.hs b/src/Extension/Data/Bounded.hs
--- a/src/Extension/Data/Bounded.hs
+++ b/src/Extension/Data/Bounded.hs
@@ -7,6 +7,7 @@
 -- Monoids for bounded types.
 module Extension.Data.Bounded (
     BoundedMax(..)
+  , BoundedMin(..)
   ) where
 
 import Data.Monoid
@@ -14,11 +15,15 @@
 -- | A newtype wrapper for a monoid of the maximum of a bounded type.
 newtype BoundedMax a = BoundedMax {getBoundedMax :: a}
     deriving( Eq, Ord, Show )
-      
+
 instance (Ord a, Bounded a) => Monoid (BoundedMax a) where
     mempty                                  = BoundedMax minBound
     (BoundedMax x) `mappend` (BoundedMax y) = BoundedMax (max x y)
 
-
+-- | A newtype wrapper for a monoid of the minimum of a bounded type.
+newtype BoundedMin a = BoundedMin {getBoundedMin :: a}
+    deriving( Eq, Ord, Show )
 
--- TODO: Add BoundedMin
+instance (Ord a, Bounded a) => Monoid (BoundedMin a) where
+    mempty                                  = BoundedMin maxBound
+    (BoundedMin x) `mappend` (BoundedMin y) = BoundedMin (min x y)
diff --git a/src/Extension/Data/ByteString.hs b/src/Extension/Data/ByteString.hs
new file mode 100644
--- /dev/null
+++ b/src/Extension/Data/ByteString.hs
@@ -0,0 +1,15 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+-- |
+-- Copyright   : (c) 2012 Benedikt Schmidt
+-- License     : GPL v3 (see LICENSE)
+-- 
+-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>
+--
+-- Provide NFData instance for ByteString
+module Extension.Data.ByteString (
+  ) where
+
+import qualified Data.ByteString as B
+import Control.DeepSeq
+
+instance NFData B.ByteString
diff --git a/src/Extension/Data/Monoid.hs b/src/Extension/Data/Monoid.hs
new file mode 100644
--- /dev/null
+++ b/src/Extension/Data/Monoid.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE CPP #-}
+-- |
+-- Copyright   : (c) 2012 Simon Meier
+-- License     : GPL v3 (see LICENSE)
+-- 
+-- Maintainer  : Simon Meier <iridcode@gmail.com>
+--
+-- A variant of "Data.Monoid" that also exports '(<>)' for 'mappend'.
+module Extension.Data.Monoid (
+    (<>)
+  , module Data.Monoid
+
+  , MinMax(..)
+  , minMaxSingleton
+  ) where
+
+import Data.Monoid
+
+#if __GLASGOW_HASKELL__ < 704
+
+infixr 6 <>
+
+-- | An infix synonym for 'mappend'.
+(<>) :: Monoid m => m -> m -> m
+(<>) = mappend
+{-# INLINE (<>) #-}
+
+#endif
+
+-- | A newtype wrapper around 'Maybe' that returns a tuple of the minimum and
+-- maximum value encountered, if there was any.
+newtype MinMax a = MinMax { getMinMax :: Maybe (a, a) }
+
+-- | Construct a 'MinMax' value from a singleton value.
+minMaxSingleton :: a -> MinMax a
+minMaxSingleton x = MinMax (Just (x, x))
+
+instance Ord a => Monoid (MinMax a) where
+    mempty = MinMax Nothing
+
+    MinMax Nothing             `mappend` y                          = y
+    x                          `mappend` MinMax Nothing             = x
+    MinMax (Just (xMin, xMax)) `mappend` MinMax (Just (yMin, yMax)) =
+       MinMax (Just (min xMin yMin, max xMax yMax))
diff --git a/src/Extension/Prelude.hs b/src/Extension/Prelude.hs
--- a/src/Extension/Prelude.hs
+++ b/src/Extension/Prelude.hs
@@ -21,7 +21,6 @@
 import System.IO
 
 
-
 -- Bool --
 ----------
 
@@ -37,18 +36,57 @@
 singleton x = [x]
 
 -- | check whether the given list contains no duplicates
+{-# INLINABLE unique #-}
 unique :: Eq a => [a] -> Bool
 unique [] = True
 unique (x:xs) = x `notElem` xs && unique xs
 
 -- | Sort list and remove duplicates. O(n*log n)
+{-# INLINE sortednub #-}
 sortednub :: Ord a => [a] -> [a]
-sortednub = map head . group . sort
+sortednub = sortednubBy compare
 
+-- | Sort a list according to a user-defined comparison function and remove
+-- duplicates.
+{-# INLINABLE sortednubBy #-}
+sortednubBy :: (a -> a -> Ordering) -> [a] -> [a]
+sortednubBy cmp = 
+    -- Adapted from GHC's Data.List module
+    -- Copyright:  (c) The University of Glasgow 2001
+    mergeAll . sequences
+  where
+    sequences (a:xs@(b:xs')) = case a `cmp` b of
+      GT -> descending b [a] xs'
+      EQ -> sequences xs
+      LT -> ascending b (a:) xs
+    sequences xs = [xs]
+
+    descending a as (b:bs)
+      | a `cmp` b == GT = descending b (a:as) bs
+    descending a as bs  = (a:as): sequences bs
+
+    ascending a as (b:bs)
+      | a `cmp` b == LT = ascending b (\ys -> as (a:ys)) bs
+    ascending a as bs   = as [a] : sequences bs
+
+    mergeAll [x] = x
+    mergeAll xs  = mergeAll (mergePairs xs)
+
+    mergePairs (a:b:xs) = merge a b: mergePairs xs
+    mergePairs xs       = xs
+
+    merge []         bs         = bs
+    merge as         []         = as
+    merge as@(a:as') bs@(b:bs') = case a `cmp` b of
+      GT -> b : merge as  bs'
+      EQ ->     merge as bs'  -- equal elements are dropped
+      LT -> a : merge as' bs
+
 -- | //O(n*log n).// Sort list and remove duplicates with respect to a
 -- projection. 
+{-# INLINE sortednubOn #-}
 sortednubOn :: Ord b => (a -> b) -> [a] -> [a]
-sortednubOn proj = map head . groupOn proj . sortOn proj
+sortednubOn proj = sortednubBy (comparing proj)
 
 -- | Keep only the first element of elements having the same projected value
 nubOn :: Eq b => (a -> b) -> [a] -> [a]
diff --git a/src/Text/Dot.hs b/src/Text/Dot.hs
--- a/src/Text/Dot.hs
+++ b/src/Text/Dot.hs
@@ -50,8 +50,10 @@
 	, mrecord_
 	) where
 
-import Data.List (intersperse)
-import Control.Monad (liftM)
+import Data.Char           (isSpace)
+import Data.List           (intersperse)
+import Control.Monad       (liftM, ap)
+import Control.Applicative (Applicative(..))
 
 data NodeId = NodeId String
 	    | UserNodeId Int
@@ -70,18 +72,35 @@
 
 data Dot a = Dot { unDot :: Int -> ([GraphElement],Int,a) }
 
+instance Functor Dot where
+  fmap f m = Dot $ \ uq -> case unDot m uq of (a,b,x) -> (a,b,f x)
+
+instance Applicative Dot where
+  pure  = return
+  (<*>) = ap
+
 instance Monad Dot where
   return a = Dot $ \ uq -> ([],uq,a)
   m >>= k  = Dot $ \ uq -> case unDot m uq of
 			   (g1,uq',r) -> case unDot (k r) uq' of
 					   (g2,uq2,r2) -> (g1 ++ g2,uq2,r2)
 
--- | 'node' takes a list of attributes, generates a new node, and gives a 'NodeId'.
-node      :: [(String,String)] -> Dot NodeId
-node attrs = Dot $ \ uq -> let nid = NodeId $ "n" ++ show uq 
-			  in ( [ GraphNode nid attrs ],succ uq,nid)
+-- | 'rawNode' takes a list of attributes, generates a new node, and gives a 'NodeId'.
+rawNode      :: [(String,String)] -> Dot NodeId
+rawNode attrs = Dot $ \ uq -> 
+    let nid = NodeId $ "n" ++ show uq 
+    in ( [ GraphNode nid attrs ],succ uq,nid)
 
+-- | 'node' takes a list of attributes, generates a new node, and gives a
+-- 'NodeId'. Multi-line labels are fixed such that they use non-breaking
+-- spaces and are terminated with a new-line.
+node :: [(String,String)] -> Dot NodeId
+node = rawNode . map fixLabel
+  where
+    fixLabel ("label",lbl) = ("label", fixMultiLineLabel lbl)
+    fixLabel attr          = attr
 
+
 -- | 'userNodeId' allows a user to use their own (Int-based) node id's, without needing to remap them.
 userNodeId :: Int -> NodeId
 userNodeId i = UserNodeId i
@@ -158,11 +177,22 @@
         showAttrs' []     = error "showAttrs: the impossible happended"
 
 showAttr :: (String, String) -> String
-showAttr (name,val) = name ++ "=\"" ++ concatMap escape val ++ "\""
-    where escape '\n' = "\\l"
-	  escape '"'  = "\\\""
-	  escape c    = [c]
+showAttr (name, val) =
+      name ++ "=\"" ++ concatMap escape val ++ "\""
+    where 
+      escape '\n' = "\\l"
+      escape '"'  = "\\\""
+      escape c    = [c]
 
+-- | Ensure that multi-line labels use non-breaking spaces at the start and
+-- are terminated with a newline.
+fixMultiLineLabel :: String -> String
+fixMultiLineLabel lbl
+  | '\n' `elem` lbl = unlines $ map useNonBreakingSpace $ lines lbl
+  | otherwise       = lbl
+  where
+    useNonBreakingSpace line = case span isSpace line of
+      (spaces, rest) -> concat (replicate (length spaces) "&nbsp;") ++ rest
 
 ------------------------------------------------------------------------------
 -- Records
@@ -177,16 +207,21 @@
   | VCat [Record a]
   deriving( Eq, Ord, Show )
 
+-- | Smart constructor for fields that massages the multi-line labels such
+-- that dot understands them.
+mkField :: Maybe a -> String -> Record a
+mkField port = Field port . fixMultiLineLabel
+
 -- | A simple field of a record.
 field :: String -> Record a
-field = Field Nothing
+field = mkField Nothing
 
 -- | A field together with a port which can be used to create direct edges to
 -- this field. Note that you can use any type to identify the ports. When
 -- creating a record node you will get back an association list between your
 -- record identifiers and their concrete node ids.
 portField :: a -> String -> Record a
-portField port = Field (Just port)
+portField port = mkField (Just port)
 
 -- | Concatenate records horizontally.
 hcat :: [Record a] -> Record a
@@ -235,11 +270,12 @@
   esc '>'  = "\\>"
   esc c    = [c]
 
+
 -- | A generic version of record creation.
 genRecord :: String -> Record a -> [(String,String)] -> Dot (NodeId, [(a,NodeId)])
 genRecord shape rec attrs = do
   (lbl, ids) <- renderRecord rec
-  i <- node ([("shape",shape),("label",lbl)] ++ attrs)
+  i <- rawNode ([("shape",shape),("label",lbl)] ++ attrs)
   return (i, ids i)
 
 -- | Create a record node with the given attributes. It returns the node-id of
diff --git a/src/Text/Isar.hs b/src/Text/Isar.hs
deleted file mode 100644
--- a/src/Text/Isar.hs
+++ /dev/null
@@ -1,319 +0,0 @@
--- |
--- Copyright   : (c) 2011 Simon Meier
--- License     : GPL v3 (see LICENSE)
--- 
--- Maintainer  : Simon Meier <iridcode@gmail.com>
--- Portability : portable
---
--- Generating Isabelle/ISAR theory files using 'Text.PrettyPrint'.
-module Text.Isar (
-    -- * ISAR Output
-    Isar(..)
-    -- ** Configuration
-  , IsarStyle(..)
-  , IsarConf(..)
-  , defaultIsarConf
-  , isPlainStyle
-  , isarPlain
-  , isarXSymbol
-
-  -- ** Constructions of our security protocol verification theory
-  , isaExecutionSystemState
-
-  -- ** Special Symbols
-  , isarightArrow
-  , isaLongRightArrow
-  , isaLParr
-  , isaRParr
-  , isaLBrack
-  , isaRBrack
-  , isaMetaAll
-  , isaExists
-  , isaAnd
-  , isaNotIn
-  , isaIn
-  , isaSubsetEq
-  , isaAlpha
-  , isaSublocale
-
-    -- * Extensions of 'Text.PrettyPrint'
-  , module Text.PrettyPrint.Class
-  , nestBetween
-  , nestShort
-  , nestShort'
-  , nestShortNonEmpty
-  , nestShortNonEmpty'
-  , fixedWidthText
-  , symbol
-  , numbered
-  , numbered'
-
-) where
-
-import Data.List
-
-import Extension.Prelude
-
-import Text.PrettyPrint.Class
-
--- | The ISAR style to be used for output.
-data IsarStyle = 
-    PlainText 
-  | XSymbol
-  deriving( Eq, Show )
-
--- | The configuration to be used for output. Apart from the ISAR style, the
--- configuration also stores the representation of the reachable state of the
--- protocol which we are reasoning about. 
-data IsarConf = IsarConf {
-    isarStyle :: IsarStyle
-  , isarTrace :: Doc        -- ^ The ISAR code of the trace
-  , isarPool  :: Doc        -- ^ The ISAR code of the thread pool
-  , isarSubst :: Doc        -- ^ The ISAR code of the substitution
-  }
-  deriving( Show )
-
--- | Default configuration: plaintext ISAR style and reachable state @(t,r,s)@.
-defaultIsarConf :: IsarConf
-defaultIsarConf = IsarConf PlainText (char 't') (char 'r') (char 's') 
-
--- | Check if the plaintext style was chosen.
-isPlainStyle :: IsarConf -> Bool
-isPlainStyle = (PlainText ==) . isarStyle
-
-
--- | Values that can be output as ISAR code. 
---
--- Minimal definition: 'isar'
-class Isar a where
-  isar :: IsarConf -> a -> Doc
-
--- | Output as ISAR code using 'defaultIsarConf'.
-isarPlain :: Isar a => a -> Doc
-isarPlain = isar defaultIsarConf
-
--- | Output as ISAR code using 'defaultIsarConf'
--- with the XSymbol style.
-isarXSymbol :: Isar a => a -> Doc
-isarXSymbol = isar (defaultIsarConf { isarStyle = XSymbol })
-
-------------------------------------------------------------------------------
--- General pretty printing combinators
-------------------------------------------------------------------------------
-
--- | Nest a document surrounded by a leading and a finishing document breaking
--- lead, body, and finish onto separate lines, if they don't fit on a single
--- line.
-nestBetween :: Document d =>
-               Int -- ^ Indent of body
-            -> d -- ^ Leading document
-            -> d -- ^ Finishing document
-            -> d -- ^ Body document
-            -> d
-nestBetween n l r x = sep [l, nest n x, r]
-
--- | Nest a document surrounded by a leading and a finishing document with an
--- non-compulsory break between lead and body.
-nestShort :: Document d =>
-             Int -- ^ Indent of body
-          -> d -- ^ Leading document
-          -> d -- ^ Finishing document
-          -> d -- ^ Body document
-          -> d
-nestShort n lead finish body = sep [lead $$ nest n body, finish]
-
--- | Nest document between two strings and indent body by @length lead + 1@.
-nestShort' :: Document d => String -> String -> d -> d
-nestShort' lead finish = 
-  nestShort (length lead + 1) (text lead) (text finish)
-
--- | Like 'nestShort' but doesn't print the lead and finish, if the document is
--- empty.
-nestShortNonEmpty :: Document d => Int -> d -> d -> d -> d
-nestShortNonEmpty n lead finish body =
-  caseEmptyDoc emptyDoc (nestShort n lead finish body) body
-
--- | Like 'nestShort'' but doesn't print the lead and finish, if the document is
--- empty.
-nestShortNonEmpty' :: Document d => String -> String -> d -> d
-nestShortNonEmpty' lead finish = 
-  nestShortNonEmpty (length lead + 1) (text lead) (text finish)
-
--- | Output text with a fixed width: if it is smaller then nothing happens,
--- otherwise care is taken to make the text appear having the given width.
-fixedWidthText :: Document d => Int -> String -> d
-fixedWidthText n cs
-  | length cs <= n  = text cs
-  | otherwise = text as <> zeroWidthText bs
-  where 
-  (as,bs) = splitAt n cs
-
--- | Print string as symbol having width 1.
-symbol :: Document d => String -> d
-symbol = fixedWidthText 1
-
--- | Number a list of documents that are vertically separated by the given
--- separator.
-numbered :: Document d => d -> [d] -> d
-numbered _   [] = emptyDoc
-numbered vsep ds = 
-    foldr1 ($-$) $ intersperse vsep $ map pp $ zip [(1::Int)..] ds
-  where
-    n         = length ds
-    nWidth    = length (show n)
-    pp (i, d) = text (flushRight nWidth (show i)) <> d
-    
--- | Number a list of documents with numbers terminated by "." and vertically
--- separate using an empty line.
-numbered' :: Document d => [d] -> d
-numbered' = numbered (text "") . map (text ". " <>)
-
-
-------------------------------------------------------------------------------
--- Operational Semantics Constructions
-------------------------------------------------------------------------------
-
--- | Isabelle representation of the exeuction system state of our operational
--- semantics.
-isaExecutionSystemState :: IsarConf -> Doc
-isaExecutionSystemState conf = 
-  parens . hcat . punctuate comma $ 
-    [isarTrace conf, isarPool conf, isarSubst conf]
-
-
-------------------------------------------------------------------------------
--- Isabelle symbols in both styles.
-------------------------------------------------------------------------------
-
--- | A 'not in' symbol: @~:@
-isaNotIn :: Document d => IsarConf -> d
-isaNotIn conf
-  | isPlainStyle conf = text "~:"
-  | otherwise         = symbol "\\<notin>"
-
--- | An 'in' symbol: @:@
-isaIn :: Document d => IsarConf -> d
-isaIn conf
-  | isPlainStyle conf  = text ":"
-  | otherwise         = symbol "\\<in>"
-
--- | A left parenthesis with an additional vertical line: @(|@
-isaLParr :: Document d => IsarConf -> d
-isaLParr conf
-  | isPlainStyle conf = text "(|"
-  | otherwise         = symbol "\\<lparr>"
-
--- | A right parenthesis with an additional vertical line: @|)@
-isaRParr :: Document d => IsarConf -> d
-isaRParr conf
-  | isPlainStyle conf = text "|)"
-  | otherwise         = symbol "\\<rparr>"
-
--- | A left bracket with an additional vertical line: @[|@
-isaLBrack :: Document d => IsarConf -> d
-isaLBrack conf
-  | isPlainStyle conf = text "[|"
-  | otherwise         = symbol "\\<lbrakk>"
-
--- | A right bracket with an additional vertical line: @|]@
-isaRBrack :: Document d => IsarConf -> d
-isaRBrack conf
-  | isPlainStyle conf = text "|]"
-  | otherwise         = symbol "\\<rbrakk>"
-
--- | A short right arrow: @->@
-isarightArrow :: Document d => IsarConf -> d
-isarightArrow conf
-  | isPlainStyle conf = text "->"
-  | otherwise         = fixedWidthText 2 "\\<rightarrow>"
-
--- | A long double right arrow: @==>@
-isaLongRightArrow :: Document d => IsarConf -> d
-isaLongRightArrow conf
-  | isPlainStyle conf = text "==>"
-  | otherwise         = fixedWidthText 3 "\\<Longrightarrow>"
-
-
--- | The greek letter alpha: @\\<alpha>@
-isaAlpha :: Document d => IsarConf -> d
-isaAlpha conf
-  | isPlainStyle conf = text "\\<alpha>"
-  | otherwise         = symbol "\\<alpha>"
-
--- | The meta all quantifier: @!!@
-isaMetaAll :: Document d => IsarConf -> d
-isaMetaAll conf
-  | isPlainStyle conf = text "!! "
-  | otherwise         = symbol "\\<And>"
-
--- | The exists symbol: @?@
-isaExists :: Document d => IsarConf -> d
-isaExists conf
-  | isPlainStyle conf = text "? "
-  | otherwise         = symbol "\\<exists>"
-
--- | The logical and symbol: @&@
-isaAnd :: Document d => IsarConf -> d
-isaAnd conf
-  | isPlainStyle conf = text "&"
-  | otherwise         = symbol "\\<and>"
-
--- | The non-strict subset symbol.
-isaSubsetEq :: Document d => IsarConf -> d
-isaSubsetEq conf
-  | isPlainStyle conf = text "<="
-  | otherwise         = symbol "\\<subseteq>"
-
--- | The sublocale sign.
-isaSublocale :: Document d => IsarConf -> d
-isaSublocale conf
-  | isPlainStyle conf = text "<"
-  | otherwise         = symbol "\\<subseteq>"
-
-------------------------------------------------------------------------------
--- Isabelle theory components
-------------------------------------------------------------------------------
-
-{- TODO: Finish, if it is used
-
-isaTheory :: Document d =>
-             String     -- ^ Theory name
-          -> [String]   -- ^ Imported theories
-          -> d          -- ^ Theory body
-          -> d          -- ^ The complete theory statement.
-isaTheory name imports body =
-  text "theory" <-> text name $-$
-  text "imports" $-$
-  nest 2 (vcat $ map (text . (++"\"") . ('"':)) imports) $-$
-  text "begin" $-$ text "" $-$
-  body $-$
-  text "" $-$ text "end"
-
-
--- | An logic identifier; properly escaped if needed.
--- TODO: Add escaping
-logicIdent :: String -> Doc
-logicIdent = text
-
-
--- | A generic text command.
-genTextCmd :: String -> String -> Doc
-genTextCmd name content = 
-  sep [text name <> text "{*", nest 2 (fsep . map text $ words content), text "*}"]
-
-chapter = genTextCmd "chapter"
-section = genTextCmd "section"
-subsection = genTextCmd "subsection"
-subsubsection = genTextCmd "subsubsection"
-paragraph = genTextCmd "text"
-
--- | A comment.
-comment :: String -> Doc
-comment content = nestShort' "(*" "*)" (fsep $ map text $ words content)
-
--- | Switch into a proof context.
-context :: String -> Doc -> Doc
-context name body = vcat [text name <-> text "begin", body, text "end"]
-
--}
-
diff --git a/src/Text/PrettyPrint/Class.hs b/src/Text/PrettyPrint/Class.hs
--- a/src/Text/PrettyPrint/Class.hs
+++ b/src/Text/PrettyPrint/Class.hs
@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
 -- |
 -- Copyright   : (c) 2011 Simon Meier
 -- License     : GPL v3 (see LICENSE)
@@ -6,18 +7,19 @@
 --
 -- 'Document' class allowing to have different interpretations of the
 -- HughesPJ pretty-printing combinators.
-{-# OPTIONS_GHC -fno-warn-orphans #-}
 module Text.PrettyPrint.Class (
         P.Doc
      ,  Document(..)
      ,  P.isEmpty
      ,  P.render
      ,  P.renderStyle
-     ,  P.style
+     ,  defaultStyle
      ,  P.Style(..)
      ,  P.Mode(..)
 
      , ($--$)
+     , emptyDoc
+     , (<>)
      , semi 
      , colon
      , comma
@@ -43,22 +45,38 @@
   
      , hang
      , punctuate
+
+     -- * Additional combinators
+     , nestBetween
+     , nestShort
+     , nestShort'
+     , nestShortNonEmpty
+     , nestShortNonEmpty'
+     , fixedWidthText
+     , symbol
+     , numbered
+     , numbered'
 ) where
 
-import Prelude
+import           Control.DeepSeq        (NFData(..))
+
+import           Data.List              (intersperse)
+
+import           Extension.Data.Monoid  (Monoid(..), (<>))
+import           Extension.Prelude      (flushRight)
+
 import qualified Text.PrettyPrint.HughesPJ as P
-import Control.DeepSeq
 
-infixl 6 <> 
-infixl 6 <->
+infixr 6 <->
 infixl 5 $$, $-$, $--$
 
-class NFData d => Document d where
+-- emptyDoc = P.empty
+-- (<>)  = (P.<>)
+
+class (Monoid d, NFData d) => Document d where
   char :: Char -> d
   text :: String -> d
   zeroWidthText :: String -> d
-  emptyDoc :: d
-  (<>)  :: d -> d -> d
   (<->) :: d -> d -> d
   hcat  :: [d] -> d
   hsep  :: [d] -> d
@@ -72,27 +90,13 @@
   nest  :: Int -> d -> d
   caseEmptyDoc :: d -> d -> d -> d
 
-instance NFData P.Doc where
-  rnf = rnf . P.render
+-- | The default 'P.Style'.
+defaultStyle :: P.Style
+defaultStyle = P.style
 
-instance Document P.Doc where
-  char = P.char
-  text = P.text
-  zeroWidthText = P.zeroWidthText
-  emptyDoc = P.empty
-  (<>)  = (P.<>)
-  (<->) = (P.<+>)
-  hcat  = P.hcat
-  hsep  = P.hsep
-  ($$)  = (P.$$)
-  ($-$) = (P.$+$)
-  vcat  = P.vcat
-  sep   = P.sep
-  cat   = P.cat
-  fsep  = P.fsep
-  fcat  = P.fcat
-  nest  = P.nest
-  caseEmptyDoc yes no d = if P.isEmpty d then yes else no
+-- | The empty document.
+emptyDoc :: Document d => d
+emptyDoc = mempty
 
 -- | Vertical concatentation of two documents with an empty line in between.
 ($--$) :: Document d => d -> d -> d
@@ -145,3 +149,99 @@
                    where
                      go d' [] = [d']
                      go d' (e:es) = (d' <> p) : go e es
+
+
+------------------------------------------------------------------------------
+-- The 'Document' instance for 'Text.PrettyPrint.Doc'
+------------------------------------------------------------------------------
+
+instance NFData P.Doc where
+  rnf = rnf . P.render
+
+instance Document P.Doc where
+  char = P.char
+  text = P.text
+  zeroWidthText = P.zeroWidthText
+  (<->) = (P.<+>)
+  hcat  = P.hcat
+  hsep  = P.hsep
+  ($$)  = (P.$$)
+  ($-$) = (P.$+$)
+  vcat  = P.vcat
+  sep   = P.sep
+  cat   = P.cat
+  fsep  = P.fsep
+  fcat  = P.fcat
+  nest  = P.nest
+  caseEmptyDoc yes no d = if P.isEmpty d then yes else no
+
+------------------------------------------------------------------------------
+-- Additional combinators
+------------------------------------------------------------------------------
+
+-- | Nest a document surrounded by a leading and a finishing document breaking
+-- lead, body, and finish onto separate lines, if they don't fit on a single
+-- line.
+nestBetween :: Document d =>
+               Int -- ^ Indent of body
+            -> d -- ^ Leading document
+            -> d -- ^ Finishing document
+            -> d -- ^ Body document
+            -> d
+nestBetween n l r x = sep [l, nest n x, r]
+
+-- | Nest a document surrounded by a leading and a finishing document with an
+-- non-compulsory break between lead and body.
+nestShort :: Document d =>
+             Int -- ^ Indent of body
+          -> d -- ^ Leading document
+          -> d -- ^ Finishing document
+          -> d -- ^ Body document
+          -> d
+nestShort n lead finish body = sep [lead $$ nest n body, finish]
+
+-- | Nest document between two strings and indent body by @length lead + 1@.
+nestShort' :: Document d => String -> String -> d -> d
+nestShort' lead finish = 
+  nestShort (length lead + 1) (text lead) (text finish)
+
+-- | Like 'nestShort' but doesn't print the lead and finish, if the document is
+-- empty.
+nestShortNonEmpty :: Document d => Int -> d -> d -> d -> d
+nestShortNonEmpty n lead finish body =
+  caseEmptyDoc emptyDoc (nestShort n lead finish body) body
+
+-- | Like 'nestShort'' but doesn't print the lead and finish, if the document is
+-- empty.
+nestShortNonEmpty' :: Document d => String -> String -> d -> d
+nestShortNonEmpty' lead finish = 
+  nestShortNonEmpty (length lead + 1) (text lead) (text finish)
+
+-- | Output text with a fixed width: if it is smaller then nothing happens,
+-- otherwise care is taken to make the text appear having the given width.
+fixedWidthText :: Document d => Int -> String -> d
+fixedWidthText n cs
+  | length cs <= n  = text cs
+  | otherwise = text as <> zeroWidthText bs
+  where
+    (as,bs) = splitAt n cs
+
+-- | Print string as symbol having width 1.
+symbol :: Document d => String -> d
+symbol = fixedWidthText 1
+
+-- | Number a list of documents that are vertically separated by the given
+-- separator.
+numbered :: Document d => d -> [d] -> d
+numbered _   [] = emptyDoc
+numbered vsep ds = 
+    foldr1 ($-$) $ intersperse vsep $ map pp $ zip [(1::Int)..] ds
+  where
+    n         = length ds
+    nWidth    = length (show n)
+    pp (i, d) = text (flushRight nWidth (show i)) <> d
+
+-- | Number a list of documents with numbers terminated by "." and vertically
+-- separate using an empty line.
+numbered' :: Document d => [d] -> d
+numbered' = numbered (text "") . map (text ". " <>)
diff --git a/src/Text/PrettyPrint/Highlight.hs b/src/Text/PrettyPrint/Highlight.hs
--- a/src/Text/PrettyPrint/Highlight.hs
+++ b/src/Text/PrettyPrint/Highlight.hs
@@ -29,13 +29,12 @@
   ) where
 
 import Text.PrettyPrint.Class
-import Control.DeepSeq
 
 -- | Currently we support only keywords, operators, and comments.
 data HighlightStyle = Keyword | Comment | Operator
        deriving( Eq, Ord, Show )
 
-class (NFData d, Document d) => HighlightDocument d where
+class Document d => HighlightDocument d where
     -- 'highlight' @style d@ marks that the document @d@ should be highlighted
     -- using the @style@.
     highlight :: HighlightStyle -> d -> d
diff --git a/src/Text/PrettyPrint/Html.hs b/src/Text/PrettyPrint/Html.hs
--- a/src/Text/PrettyPrint/Html.hs
+++ b/src/Text/PrettyPrint/Html.hs
@@ -31,6 +31,7 @@
 
 import Data.Char (isSpace)
 import Data.Traversable (sequenceA)
+import Data.Monoid
 
 import Control.Arrow (first)
 import Control.Applicative
@@ -89,6 +90,7 @@
 
 -- | A 'Document' transformer that adds proper HTML escaping.
 newtype HtmlDoc d = HtmlDoc { getHtmlDoc :: d }
+    deriving( Monoid )
 
 -- | Wrap a document such that HTML markup can be added without disturbing the
 -- layout.
@@ -102,9 +104,7 @@
     char          = HtmlDoc . text . escapeHtmlEntities . return
     text          = HtmlDoc . text . escapeHtmlEntities 
     zeroWidthText = HtmlDoc . zeroWidthText . escapeHtmlEntities
-    emptyDoc      = HtmlDoc emptyDoc
 
-    HtmlDoc d1 <>  HtmlDoc d2 = HtmlDoc $ d1 <> d2
     HtmlDoc d1 <-> HtmlDoc d2 = HtmlDoc $ d1 <-> d2
     hcat = HtmlDoc . hcat . map getHtmlDoc
     hsep = HtmlDoc . hsep . map getHtmlDoc
@@ -170,6 +170,7 @@
 newtype NoHtmlDoc d = NoHtmlDoc { unNoHtmlDoc :: Identity d }
   deriving( Functor, Applicative )
 
+
 -- | Wrap a document such that all 'HtmlDocument' specific methods are ignored.
 noHtmlDoc :: d -> NoHtmlDoc d
 noHtmlDoc = NoHtmlDoc . Identity
@@ -181,12 +182,14 @@
 instance NFData d => NFData (NoHtmlDoc d) where
     rnf = rnf . getNoHtmlDoc
 
+instance Monoid d => Monoid (NoHtmlDoc d) where
+  mempty = pure mempty
+  mappend = liftA2 mappend
+
 instance Document d => Document (NoHtmlDoc d) where
   char = pure . char
   text = pure . text
   zeroWidthText = pure . zeroWidthText
-  emptyDoc = pure emptyDoc
-  (<>)  = liftA2 (<>)
   (<->) = liftA2 (<->)
   hcat  = liftA hcat . sequenceA
   hsep  = liftA hsep . sequenceA
diff --git a/src/Utils/Misc.hs b/src/Utils/Misc.hs
--- a/src/Utils/Misc.hs
+++ b/src/Utils/Misc.hs
@@ -1,12 +1,7 @@
 {-# LANGUAGE DeriveDataTypeable, RankNTypes, ScopedTypeVariables, BangPatterns #-}
 module Utils.Misc (
-    invertMap
-
-  , pNat
-  , commaWS
-
   -- * Environment
-  , envIsSet
+    envIsSet
   , getEnvMaybe
 
   -- * List operations
@@ -19,19 +14,23 @@
 
   -- * Hashing
   , stringSHA256
+
+  -- * Set operations
+  , setAny
+
+  -- * Map operations
+  , invertMap
 ) where
 
 import Data.List
 import System.Environment
 import System.IO.Unsafe
 import Data.Maybe
+import Data.Set (Set)
 import qualified Data.Set as S
 import Data.Map ( Map )
 import qualified Data.Map as M
-import Control.Applicative
 
-import Text.ParserCombinators.Parsec hiding (many, optional, (<|>))
-
 import Data.Digest.Pure.SHA      (bytestringDigest, sha256)
 import Blaze.ByteString.Builder  (toLazyByteString)
 import qualified Data.ByteString.Char8              as C8
@@ -61,14 +60,6 @@
 invertMap :: (Ord k, Ord v) => Map k v -> Map v k
 invertMap = M.fromList . map (uncurry (flip (,))) . M.toList
 
--- | parse natural number
-pNat :: GenParser Char st Int
-pNat = read <$> many1 digit
-
--- | parse comma
-commaWS :: GenParser Char st ()
-commaWS = char ',' *> spaces
-
 -- | @whileTrue m@ iterates m until it returns @False@.
 --   Returns the number of iterations @m@ was run. @0@
 --   means @m@ never returned @True@.
@@ -93,3 +84,6 @@
    replace '/' = '_'
    replace '+' = '-'
    replace c   = c
+
+setAny :: (a -> Bool) -> Set a -> Bool
+setAny f = S.foldr (\x b -> f x || b) False
diff --git a/tamarin-prover-utils.cabal b/tamarin-prover-utils.cabal
--- a/tamarin-prover-utils.cabal
+++ b/tamarin-prover-utils.cabal
@@ -2,7 +2,7 @@
 
 cabal-version:      >= 1.8
 build-type:         Simple
-version:            0.1.0.0
+version:            0.4.0.0
 license:            GPL
 license-file:       LICENSE
 category:           Theorem Provers
@@ -13,7 +13,7 @@
 
 synopsis:           Utility library for the tamarin prover.
 
-description:        This is an internal library of the @tamarin@ prover for
+description:        This is an internal library of the Tamarin prover for
                     security protocol verification
                     (<hackage.haskell.org/package/tamarin-prover>). 
 
@@ -25,28 +25,34 @@
 ----------------------
 
 library
+    ghc-prof-options:  -auto-all
+
     build-depends:
         base              == 4.*
       , mtl               == 2.0.*
+      , bytestring        == 0.9.*
       , transformers      == 0.2.*
-      , containers        == 0.4.*
-      , fclabels          == 1.0.*
+      , containers        >= 0.4.2   && < 0.5
+      , fclabels          == 1.1.*
       , blaze-builder     == 0.3.*
       , base64-bytestring >= 0.1.0.3 && < 0.2
       , bytestring        == 0.9.*
-      , SHA               == 1.4.*
+      , SHA               == 1.5.*
       , parsec            == 3.1.*
-      , deepseq           == 1.1.*
+      , deepseq           == 1.3.*
       , syb               >= 0.3.3   && < 0.4
       , pretty            == 1.1.*
-      , time              == 1.2.*
+      , time              >= 1.2     && < 1.5
       , binary            == 0.5.*
+      , dlist             == 0.5.*
 
     hs-source-dirs: src
 
     exposed-modules:
         Control.Basics
         Control.Monad.Fresh
+        Control.Monad.Trans.PreciseFresh
+        Control.Monad.Trans.FastFresh
         Control.Monad.Bind
         Control.Monad.Disj
 
@@ -55,10 +61,11 @@
 
         Extension.Prelude
         Extension.Data.Label
+        Extension.Data.Monoid
         Extension.Data.Bounded
+        Extension.Data.ByteString
 
         Text.Dot
-        Text.Isar
         Text.PrettyPrint.Class
         Text.PrettyPrint.Highlight
         Text.PrettyPrint.Html
@@ -72,7 +79,6 @@
         Utils.Misc
 
     other-modules:
-        Control.Monad.Trans.Fresh
         Control.Monad.Fresh.Class
 
         Control.Monad.Trans.Disj