diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.2.19
+Version: 0.2.20
 Cabal-version: >= 1.8
 Build-type: Simple
 Author: Nick Smallbone
diff --git a/src/Jukebox/Clausify.hs b/src/Jukebox/Clausify.hs
--- a/src/Jukebox/Clausify.hs
+++ b/src/Jukebox/Clausify.hs
@@ -23,7 +23,8 @@
   inGroup "Input and clausifier options" $
   ClausifyFlags <$>
     bool "split"
-      ["Split the conjecture into several sub-conjectures."]
+      ["Split the conjecture into several sub-conjectures (off by default)."]
+      False
 
 ----------------------------------------------------------------------
 -- clausify
@@ -39,7 +40,9 @@
     do cs <- clausForm axiom inp
        clausifyInputs (cs ++ theory) obligs inps
 
-  clausifyInputs theory obligs (inp:inps) | kind inp `elem` [Conjecture, Question] =
+  clausifyInputs theory obligs (inp:inps)
+      -- XX translate question in answer literal
+    | Conjecture _ <- kind inp =
     do clausifyObligs theory obligs inp (split' (what inp)) inps
 
   clausifyObligs theory obligs _ [] inps =
diff --git a/src/Jukebox/Form.hs b/src/Jukebox/Form.hs
--- a/src/Jukebox/Form.hs
+++ b/src/Jukebox/Form.hs
@@ -307,7 +307,7 @@
 
 type Tag = String
 
-data Kind = Axiom String | Conjecture | Question deriving (Eq, Ord)
+data Kind = Axiom String | Conjecture String deriving (Eq, Ord)
 
 data Answer = Sat SatReason | Unsat UnsatReason | NoAnswer NoAnswerReason
   deriving (Eq, Ord)
diff --git a/src/Jukebox/Monotonox/ToFOF.hs b/src/Jukebox/Monotonox/ToFOF.hs
--- a/src/Jukebox/Monotonox/ToFOF.hs
+++ b/src/Jukebox/Monotonox/ToFOF.hs
@@ -43,7 +43,7 @@
         aux _pos (Equiv _ _) = error "ToFOF.guard: equiv should have been eliminated"
         aux _pos (Connective _ _ _) = error "ToFOF.guard: connective should have been eliminated"
         pos Axiom{} = True
-        pos Conjecture = False
+        pos Conjecture{} = False
 
 translate, translate1 :: Scheme -> (Type -> Bool) -> Problem Form -> Problem Form
 translate1 scheme mono f = Form.run f $ \inps -> do
@@ -77,7 +77,7 @@
               Axiom{} ->
                 fmap (Input tag kind (Inference "type_encoding" "esa" [inp])) $
                   prepare f
-              Conjecture ->
+              Conjecture{} ->
                 fmap (Input tag kind (Inference "type_encoding" "esa" [inp])) $
                 fmap notInwards $ prepare $ nt f
       typeI = Type (name "$i") (Finite 0) Infinite
@@ -91,8 +91,9 @@
 tagsFlags =
   inGroup "Options for encoding types" $
   bool "more-axioms"
-    ["Add extra, redundant typing axioms for function arguments.",
+    ["Add extra, redundant typing axioms for function arguments (off by default).",
      "May help or hinder the prover. Only affects --encoding tags."]
+    False
 
 tags :: Bool -> Scheme
 tags moreAxioms = Scheme
diff --git a/src/Jukebox/Options.hs b/src/Jukebox/Options.hs
--- a/src/Jukebox/Options.hs
+++ b/src/Jukebox/Options.hs
@@ -40,7 +40,7 @@
 ----------------------------------------------------------------------
 -- The ArgParser type: parsing of single flags.
 
-type ArgParser = Annotated String SeqParser
+type ArgParser = Annotated [String] SeqParser
   -- annotated with a description, e.g. "<number>"
 
 -- Called SeqParser because <*> is sequential composition.
@@ -60,7 +60,7 @@
 -- Combinators for building ArgParsers.
 
 arg :: String -> String -> (String -> Maybe a) -> ArgParser a
-arg desc err f = Annotated desc (SeqParser 1 c)
+arg desc err f = Annotated [desc] (SeqParser 1 c)
   where c [] = Left (Mistake err)
         c (x:_) | "-" `isPrefixOf` x = Left (Mistake err)
         c (x:_) =
@@ -131,9 +131,14 @@
 data Flag = Flag
   { flagName :: String,
     flagGroup :: String,
+    flagMode :: FlagMode,
     flagHelp :: [String],
     flagArgs :: String } deriving (Eq, Show)
+data FlagMode = NormalMode | ExpertMode | HiddenMode deriving (Eq, Show)
 
+flagExpert :: Flag -> Bool
+flagExpert f = flagMode f == ExpertMode
+
 -- Called ParParser because <*> is parallel composition.
 -- In other words, in f <*> x, f and x both see the whole command line.
 -- We want this when parsing command lines because
@@ -185,57 +190,72 @@
     No _ -> Left (Mistake ("Didn't recognise option " ++ x))
     Error err -> Left err
 
-awaitP :: (String -> Bool) -> a -> (String -> [String] -> ParseResult a) -> ParParser a
-awaitP p def par = ParParser (return def) f
+await :: (String -> Bool) -> a -> (String -> [String] -> ParseResult a) -> ParParser a
+await p def par = ParParser (return def) f
   where f (x:xs) | p x =
           case par x xs of
             Yes n r -> Yes (n+1) r
             No _ ->
               error "Options.await: got No"
             Error err -> Error err
-        f _ = No (awaitP p def par)
+        f _ = No (await p def par)
 
-await :: String -> a -> ([String] -> ParseResult a) -> ParParser a
-await flag def f = awaitP (\x -> "--" ++ flag == x) def (const f)
+----------------------------------------------------------------------
+-- Low-level primitives for building OptionParsers.
 
+-- Produce an OptionParser with maximum flexibility.
+primFlag ::
+  -- Name and description of options (for documentation)
+  String -> [String] ->
+  -- Predicate which checks if this argument is our option
+  (String -> Bool) ->
+  -- Handle repeated occurrences of the same option
+  (a -> a -> Either Error a) ->
+  -- Default argument value and argument parser
+  -- The argument parser is given the option name.
+  a -> ArgParser (String -> a) -> OptionParser a
+primFlag name help p combine def (Annotated desc (SeqParser args f)) =
+  Annotated [desc'] (await p def (g Right))
+  where desc' = Flag name "General options" NormalMode help (unwords desc)
+        g comb x xs =
+          case f xs >>= comb . ($ x) of
+            Left (Mistake err) -> Error (Mistake ("Error in option --" ++ name ++ ": " ++ err))
+            Left (Usage code err) -> Error (Usage code err)
+            Right y ->
+              Yes args (await p y (g (combine y)))
+
 ----------------------------------------------------------------------
 -- Combinators for building OptionParsers.
 
 -- From a flag name and description and argument parser, produce an OptionParser.
 flag :: String -> [String] -> a -> ArgParser a -> OptionParser a
-flag name help def (Annotated desc (SeqParser args f)) =
-  Annotated [desc'] (await name def g)
-  where desc' = Flag name "General options" help desc
-        g xs =
-          case f xs of
-            Left (Mistake err) -> Error (Mistake ("Error in option --" ++ name ++ ": " ++ err))
-            Left (Usage code err) -> Error (Usage code err)
-            Right y -> Yes args (pure y <* noFlag)
-        -- Give an error if the flag is repeated.
-        noFlag =
-          await name ()
-            (const (Error (Mistake ("Option --" ++ name ++ " occurred twice"))))
-
--- A boolean flag.
-bool :: String -> [String] -> OptionParser Bool
-bool name help = flag name help False (pure True)
+flag name help def p =
+  primFlag name help
+    (\x -> x == "--" ++ name)
+    (\x y -> return y) -- take second occurrence of flag
+    def (const <$> p)
 
 -- A variant of 'flag' that allows repeated flags.
 manyFlags :: String -> [String] -> ArgParser a -> OptionParser [a]
-manyFlags name help (Annotated desc (SeqParser args f)) =
-  fmap reverse (Annotated [desc'] (go []))
-  where desc' = Flag name "Common options" help desc
-        go xs = await name xs (g xs)
-        g xs ys =
-          case f ys of
-            Left (Mistake err) -> Error (Mistake ("Error in option --" ++ name ++ ": " ++ err))
-            Left (Usage code err) -> Error (Usage code err)
-            Right x -> Yes args (go (x:xs))
+manyFlags name help p =
+  primFlag name help
+    (\x -> x == "--" ++ name)
+    (\x y -> return (x ++ y))
+    [] (const <$> return <$> p)
 
+-- A boolean flag.
+bool :: String -> [String] -> Bool -> OptionParser Bool
+bool name help def =
+  primFlag ("(no-)" ++ name) help
+    (\x -> x `elem` ["--" ++ name, "--no-" ++ name])
+    (\x y -> return y)
+    def
+    (pure (\name' -> if "--" ++ name == name' then True else False))
+
 -- A parser that reads all file names from the command line.
 filenames :: OptionParser [String]
 filenames = Annotated [] (from [])
-  where from xs = awaitP p xs (f xs)
+  where from xs = await p xs (f xs)
         p x = not ("-" `isPrefixOf` x) || x == "-"
         f xs y _ = Yes 0 (from (xs ++ [y]))
 
@@ -248,6 +268,14 @@
 inGroup :: String -> OptionParser a -> OptionParser a
 inGroup x (Annotated fls f) = Annotated [fl{ flagGroup = x } | fl <- fls] f
 
+-- Mark a flag as being for experts only.
+expert :: OptionParser a -> OptionParser a
+expert (Annotated fls f) = Annotated [fl{ flagMode = ExpertMode } | fl <- fls] f
+
+-- Mark a flag as being hidden.
+hidden :: OptionParser a -> OptionParser a
+hidden (Annotated fls f) = Annotated [fl{ flagMode = HiddenMode } | fl <- fls] f
+
 -- Add a --version flag.
 version :: String -> OptionParser a -> OptionParser a
 version x p =
@@ -275,25 +303,40 @@
     p' =
       p <*
         (inGroup "Miscellaneous options" $
-         flag "help" ["Show this help text."] () (argUsage ExitSuccess (helpText name description p')))
+         flag "help" ["Show help text."] ()
+        
+           (argUsage ExitSuccess (helpText False name description p')))
+        <*
+        (if any flagExpert (descr p) then
+          (inGroup "Miscellaneous options" $
+           flag "expert-help" ["Show help text for hidden options."] ()
+             (argUsage ExitSuccess (helpText True name description p')))
+         else pure ())
 
 usageText :: String -> String -> [String]
 usageText name descr =
   [descr ++ ".",
-   "Usage: " ++ name ++ " <option>* <file>*, where <file> should be in TPTP format."]
+   "Usage: " ++ name ++ " <option>* <file>*, where <file> is in TPTP format."]
 
-helpText :: String -> String -> OptionParser a -> [String]
-helpText name description p =
+helpText :: Bool -> String -> String -> OptionParser a -> [String]
+helpText expert name description p =
   intercalate [""] $
     [usageText name description] ++
     [[flagGroup f0 ++ ":"] ++
      concat [justify ("--" ++ flagName f ++ " " ++ flagArgs f) (flagHelp f) | f <- fs]
-     | fs@(f0:_) <- groups (nub (descr p)) ]
+     | fs@(f0:_) <- groups (filter ok (nub (descr p))) ] ++
+    [ ["To see hidden options too, try --expert-help."]
+    | any flagExpert (descr p), not expert ]
   where
     groups [] = []
     groups (f:fs) =
       (f:[f' | f' <- fs, flagGroup f == flagGroup f']):
       groups [f' | f' <- fs, flagGroup f /= flagGroup f']
+    ok flag =
+      case flagMode flag of
+        NormalMode -> True
+        ExpertMode -> expert
+        HiddenMode -> False
 
 justify :: String -> [String] -> [String]
 justify name help = ["  " ++ name] ++ map ("    " ++) help
diff --git a/src/Jukebox/Provers/E.hs b/src/Jukebox/Provers/E.hs
--- a/src/Jukebox/Provers/E.hs
+++ b/src/Jukebox/Provers/E.hs
@@ -25,18 +25,15 @@
   inGroup "E prover options" $
   EFlags <$>
     flag "eprover"
-      ["Path to the E theorem prover.",
-       "Default: eprover"]
+      ["Path to the E theorem prover (\"eprover\" by default)."]
       "eprover"
       argFile <*>
     flag "timeout"
-      ["Timeout for E, in seconds.",
-       "Default: (off)"]
+      ["Timeout for E, in seconds (off by default)."]
       Nothing
       (fmap Just argNum) <*>
     flag "memory"
-      ["Memory limit for E, in megabytes.",
-       "Default: (off)"]
+      ["Memory limit for E, in megabytes (unlimited by default)."]
       Nothing
       (fmap Just argNum)
 
diff --git a/src/Jukebox/Provers/SPASS.hs b/src/Jukebox/Provers/SPASS.hs
--- a/src/Jukebox/Provers/SPASS.hs
+++ b/src/Jukebox/Provers/SPASS.hs
@@ -19,18 +19,15 @@
   inGroup "SPASS prover options" $
   SPASSFlags <$>
     flag "spass"
-      ["Path to SPASS.",
-       "Default: SPASS"]
+      ["Path to SPASS (\"SPASS\" by default)."]
       "SPASS"
       argFile <*>
     flag "timeout"
-      ["Timeout in seconds.",
-       "Default: (none)"]
+      ["Timeout in seconds (off by default)."]
       Nothing
       (fmap Just argNum) <*>
     flag "sos"
-      ["Use set-of-support strategy.",
-       "Default: false"]
+      ["Use set-of-support strategy (off by default)."]
       False
       (pure True)
 
diff --git a/src/Jukebox/SMTLIB.hs b/src/Jukebox/SMTLIB.hs
--- a/src/Jukebox/SMTLIB.hs
+++ b/src/Jukebox/SMTLIB.hs
@@ -185,9 +185,7 @@
 pPrintInput :: Input Form -> Doc
 pPrintInput Input{kind = Axiom _, what = form} =
   sexp ["assert", pPrintForm form]
-pPrintInput Input{kind = Conjecture, what = form} =
-  sexp ["assert", sexp ["not", pPrintForm form]]
-pPrintInput Input{kind = Question, what = form} =
+pPrintInput Input{kind = Conjecture _, what = form} =
   sexp ["assert", sexp ["not", pPrintForm form]]
 
 pPrintForm :: Form -> Doc
diff --git a/src/Jukebox/TPTP/FindFile.hs b/src/Jukebox/TPTP/FindFile.hs
--- a/src/Jukebox/TPTP/FindFile.hs
+++ b/src/Jukebox/TPTP/FindFile.hs
@@ -36,9 +36,9 @@
   concat <$>
   sequenceA [
     pure ["."],
-    flag "root"
-      ["Extra directories that will be searched for TPTP input files."]
-      []
-      argFiles,
+    concat <$>
+      manyFlags "root"
+        ["Extra directories that will be searched for TPTP input files."]
+        argFiles,
     io getTPTPDirs
     ]
diff --git a/src/Jukebox/TPTP/Parse/Core.hs b/src/Jukebox/TPTP/Parse/Core.hs
--- a/src/Jukebox/TPTP/Parse/Core.hs
+++ b/src/Jukebox/TPTP/Parse/Core.hs
@@ -25,7 +25,7 @@
    keyword, defined, kind)
 import qualified Jukebox.TPTP.Lexer as L
 import qualified Jukebox.Form as Form
-import Jukebox.Form hiding (tag, kind, Axiom, Conjecture, Question, newFunction, TypeOf(..), run, Theorem)
+import Jukebox.Form hiding (tag, kind, Axiom, Conjecture, newFunction, TypeOf(..), run, Theorem)
 import qualified Jukebox.Name as Name
 
 -- The parser monad
@@ -268,8 +268,8 @@
   axiom Axiom <|> axiom Hypothesis <|> axiom Definition <|>
     axiom Assumption <|> axiom Lemma <|> axiom Theorem <|>
     axiom NegatedConjecture <|>
-    general Conjecture Form.Conjecture <|>
-    general Question Form.Question
+    general Conjecture (Form.Conjecture "conjecture") <|>
+    general Question (Form.Conjecture "question")
 
 -- A formula name.
 tag :: Parser Tag
@@ -329,7 +329,7 @@
                  else
                    " has type " ++ showTypes (map rhs fs) ++
                    " but was applied to " ++ plural (length args') "an argument" "arguments" ++
-                   " of type " ++ prettyShow (map typ args')
+                   " of type " ++ intercalate ", " (map (prettyShow . typ) args')
 
 {-# INLINE lookupType #-}
 lookupType :: String -> Parser Type
diff --git a/src/Jukebox/TPTP/Print.hs b/src/Jukebox/TPTP/Print.hs
--- a/src/Jukebox/TPTP/Print.hs
+++ b/src/Jukebox/TPTP/Print.hs
@@ -298,8 +298,7 @@
 
 instance Show Kind where
   show (Axiom kind) = kind
-  show Conjecture = "conjecture"
-  show Question = "question"
+  show (Conjecture kind) = kind
 
 prettyNames :: Symbolic a => a -> a
 prettyNames x0 = mapName replace x
diff --git a/src/Jukebox/Toolbox.hs b/src/Jukebox/Toolbox.hs
--- a/src/Jukebox/Toolbox.hs
+++ b/src/Jukebox/Toolbox.hs
@@ -35,8 +35,11 @@
 globalFlags =
   inGroup "Output options" $
   GlobalFlags <$>
-    bool "quiet"
-      ["Do not print any informational output."]
+    -- Use flag rather than bool to avoid getting a --no-quiet option in the
+    -- help message
+    flag "quiet"
+      ["Only print essential information."]
+      False (pure True)
 
 data TSTPFlags =
   TSTPFlags {
@@ -48,7 +51,8 @@
   inGroup "Output options" $
   TSTPFlags <$>
     bool "tstp"
-      ["Produce TSTP-friendly output."]
+      ["Produce TSTP-compatible output (off by default)."]
+      False
 
 ----------------------------------------------------------------------
 -- Printing output messages.
@@ -122,7 +126,7 @@
 writeFileBox =
   inGroup "Output options" $
   flag "output"
-    ["Where to write the output file (defaults to stdout)."]
+    ["Where to write the output file (stdout by default)."]
     putStr
     (fmap myWriteFile argFile)
   where myWriteFile "/dev/null" _ = return ()
@@ -145,8 +149,8 @@
     flags =
       inGroup "Input and clausifier options" $
       flag "conjecture"
-        ["If the problem has multiple conjectures, take only this one",
-         "(conjectures are numbered from 1)"]
+        ["If the problem has multiple conjectures, take only this one.",
+         "Conjectures are numbered from 1."]
         Nothing (Just <$> argNum)
 
 oneConjecture :: Maybe Int -> CNF -> IO (Problem Clause)
@@ -236,7 +240,7 @@
   inGroup "Options for encoding types" $
   choose <$>
   flag "encoding"
-    ["Which type encoding to use (defaults to guards)."]
+    ["Which type encoding to use (guards by default)."]
     "guards"
     (argOption ["guards", "tags"])
   <*> tagsFlags
@@ -276,7 +280,7 @@
     <$> expansive <*> universe
   where universe = choose <$>
                    flag "universe"
-                   ["Which universe to find the model in (defaults to peano)."]
+                   ["Which universe to find the model in (peano by default)."]
                    "peano"
                    (argOption ["peano", "trees"])
         choose "peano" = Peano