sig
  type trs
  val syntax_defs_of_sys : TRS.trs -> (string * SyntaxDef.syntax_def) list
  val set_vals_of_sys : TRS.trs -> (string * Term.term * Term.term) list
  val update_on_term : string -> Term.term -> TRS.trs -> TRS.trs
  val normalise_with_sys : TRS.trs -> Term.term -> Term.term
  val parse_with_sys : TRS.trs -> string -> Term.term list
  val parse_disambiguate_with_sys :
    bool -> TRS.trs -> string -> Term.term list
  val message_for_term :
    Term.decls_set ->
    (string * SyntaxDef.syntax_def) list ->
    string -> bool -> bool -> Term.term * Term.term -> string
  exception FAILED_PARSE_OR_EXN of string
  val process_with_system :
    string ->
    bool ->
    TRS.trs ->
    string -> bool -> (string -> unit) -> TRS.trs * Term.term list * string
  val basic_system : (unit -> TRS.trs) Pervasives.ref
  val step_shell :
    string ->
    bool ->
    TRS.trs ->
    (unit -> char) ->
    bool -> Term.term list Pervasives.ref -> (string -> unit) -> TRS.trs
  val run_shell :
    string ->
    bool ->
    TRS.trs Pervasives.ref ->
    (unit -> char) ->
    bool -> Term.term list Pervasives.ref -> (string -> unit) -> unit
  val run_shell_str :
    ?libpath:string ->
    ?sys:TRS.trs -> string -> string * TRS.trs * Term.term list
end