let commands () =
  Format.eprintf "@[";
  Format.eprintf "assert <atom>.            Assert atom in current context.@\n";
  Format.eprintf "can <term>.               Canonical forms.@\n";
  Format.eprintf "ctxt.                     Current logical context.@\n";
  Format.eprintf "def <var> := <term>.      Term definition.@\n"; 
  Format.eprintf "diseq <term>.             Variables known to be disequal.@\n";
  Format.eprintf "dom <term>.               Domain of interpretation@\n";
  Format.eprintf "exit.                     Exiting ICS interpreter (or: Ctrl-D)@\n";
  Format.eprintf "forget.                   Clearing current logical context.@\n";
  Format.eprintf "find <th> <var>.          Interpretation of variable in theory.@\n";
  Format.eprintf "help [commands | syntax]. Help texts.@\n";
  Format.eprintf "inv <th> <term>.          External variable for term in theory@\n";
  Format.eprintf "prop <var> := <prop>.     Definition for a proposition.@\n"; 
  Format.eprintf "reset.                    Reinitializing ICS.@\n";
  Format.eprintf "restore <name>.           Restore current context.@\n";
  Format.eprintf "remove <name>.            Remove a saved current context.@\n";
  Format.eprintf "save <name>.              Save current context.@\n";
  Format.eprintf "sat <prop>.               Propositional satisfiability@\n";
  Format.eprintf "sig <var> : bv[<int>].    Signature for bitvector variables.@\n";
  Format.eprintf "sig <var> : [dom | real]. Signature for arithmetic variables.@\n";
  Format.eprintf "sigma (<term> | <atom>).  Normal forms.@\n";
  Format.eprintf "sign <term>.              Abstrat sign interpretation of a term.@\n";
  Format.eprintf "show.                     Solution sets and variable partitioning.@\n";
  Format.eprintf "solve <ith> <term> = <term>. Solve equation in interpreted theory.@\n";
  Format.eprintf "symtab [<name>].          Symbol table entries.@\n";
  Format.eprintf "trace <ident>,...,<ident>. Tracing.@\n"; 
  Format.eprintf "unsat <prop>.             Check for unsatisfiability.@\n";
  Format.eprintf "untrace.                  Stop tracing.@\n";
  Format.eprintf "use <th> <var>.           Occurrences of variables.@\n";
  Format.eprintf "valid <prop>.             Validity check.@\n";
  Format.eprintf "An interpreted theory <ith> is either 'a' for arithmetic, 't' for@\n";
  Format.eprintf "tuples, or 'bv' for bitvectors. In addition, <th> includes 'u' the@\n";
  Format.eprintf "theory of unintepreted terms";
  Format.eprintf "@]@."