diff --git a/ftshell.cabal b/ftshell.cabal
--- a/ftshell.cabal
+++ b/ftshell.cabal
@@ -1,5 +1,5 @@
 name:           ftshell
-version:        0.2
+version:        0.3
 license:        PublicDomain
 license-file:   LICENSE
 author:         Sascha Boehme
@@ -11,19 +11,27 @@
     that library to generate free theorems from Haskell type
     expressions.
 category:       Language, Source-tools
-tested-with: 	GHC==6.8.2
-build-type:	Simple
+tested-with:    GHC==6.8.2
+build-type:     Simple
 build-depends:
     base >= 1.0
   , mtl >= 1.0
   , Shellac >= 0.9
   , Shellac-readline >= 0.9
-  , free-theorems >= 0.2
+  , free-theorems >= 0.3
   , pretty >= 1.0.0.0
   , containers >= 0.1.0.1
 data-files:
     declarations.hs
+    README
 executable:     ftshell
 main-is:        main.hs
+other-modules: 
+        Shell
+        Evaluate
+        Settings
+        Commands
+        ShellState
+        HelpCommands
 hs-source-dirs: src
 extensions: MultiParamTypeClasses
diff --git a/src/Commands.hs b/src/Commands.hs
--- a/src/Commands.hs
+++ b/src/Commands.hs
@@ -276,7 +276,13 @@
 cmdShowTheorem :: Sh ShellState ()
 cmdShowTheorem = withCurrentContext $ \sig intermediate -> do
   opts <- fromShellSt getCurrentTheoremOptions
-  let pt = prettyTheorem opts (asTheorem intermediate)
+  simp <- fromShellSt getSimplifyOutput
+  l <- fromShellSt getCurrentLanguageSubset
+  let pt = prettyTheorem opts $
+           (if simp && l `elem` [BasicSubset, SubsetWithFix EquationalTheorem]
+           then simplify
+           else id) $
+           asTheorem intermediate
   shellPutStrLn "The free theorem for the type signature\n"
   (shellPutStrLn . doRender 2 . prettySignature . rawSignature) sig
   l <- fromShellSt getCurrentLanguageSubset
@@ -291,12 +297,17 @@
 cmdShowLiftedRelations = withCurrentContext $ \_ intermediate -> do
   vds  <- fromShellSt (concat . Map.elems . getAllDeclarations)
   opts <- fromShellSt getCurrentTheoremOptions
+  simp <- fromShellSt getSimplifyOutput
+  l <- fromShellSt getCurrentLanguageSubset
+  let simpL = if simp && l `elem` [BasicSubset, SubsetWithFix EquationalTheorem]
+	      then simplifyUnfoldedLift
+              else id
   let lifts = unfoldLifts vds intermediate
   if null lifts
     then shellPutStrLn "There are no lifted relations in the current theorem."
     else do shellPutStrLn ""
             mapM_ (\s -> shellPutStrLn (s ++ "\n"))
-                  (map (doRender 2 . prettyUnfoldedLift opts) lifts)
+                  (map (doRender 2 . prettyUnfoldedLift opts . simpL) lifts)
 
 
 
@@ -408,6 +419,9 @@
   opts <- fromShellSt getCurrentTheoremOptions
   shellPutStrLn "The current options for displaying theorems are:"
   mapM_ (showOpt opts) (Map.keys allTheoremOptions)
+  simp <- fromShellSt getSimplifyOutput
+  if simp then shellPutStrLn "The output will be simplified, if possible."
+          else shellPutStrLn "The output will not be simplified."
   where
     showOpt opts o =
       if fromJust (Map.lookup o allTheoremOptions) `elem` opts
@@ -430,7 +444,14 @@
   let add opt os = if opt `notElem` os then opt : os else os
    in updateTheoremOptions add
 
-
+-- Toggles the simplify output flag
+cmdToggleSimplify :: Sh ShellState ()
+cmdToggleSimplify = do
+  modifyShellSt $ \s -> s { getSimplifyOutput = not (getSimplifyOutput s) }
+  simp <- fromShellSt getSimplifyOutput
+  if simp then shellPutStrLn "The output will be simplified, if possible."
+          else shellPutStrLn "The output will not be simplified."
+  
 
 -- Modifies the current theorem options with the help of a modification
 -- function.
diff --git a/src/Shell.hs b/src/Shell.hs
--- a/src/Shell.hs
+++ b/src/Shell.hs
@@ -191,7 +191,10 @@
         "Turn on a theorem option"
 
   , cmd "omit" cmdTheoremOptionOmit
-        "Turn off a theorem option\n"
+        "Turn off a theorem option"
+
+  , cmd "toggle-simplify" cmdToggleSimplify
+	"Toggle whether the theorems are simplified\n"
   
   , exitCommand "quit"
   ]
diff --git a/src/ShellState.hs b/src/ShellState.hs
--- a/src/ShellState.hs
+++ b/src/ShellState.hs
@@ -76,6 +76,9 @@
   , getCurrentTheoremOptions :: [PrettyTheoremOption]
         -- The current options which modify how theorems are pretty-printed.
 
+  , getSimplifyOutput :: Bool
+	-- Whether the Theorems.Simplify module should be used (if allowed by the
+	-- language subtype)
   }
 
 
@@ -95,6 +98,7 @@
   , getCurrentTheoremOptions = [ OmitTypeInstantiations
                                -- , OmitLanguageSubsets
                                ]
+  , getSimplifyOutput        = True
   }
 
 
@@ -112,6 +116,7 @@
   , getCurrentContext        = Nothing
   , getSpecialisationHistory = []
   , getCurrentTheoremOptions = getCurrentTheoremOptions state
+  , getSimplifyOutput        = True
   }