1signature smlExecute =
2sig
3
4  include Abbrev
5
6  (* execution function *)
7  val quse_string : string -> bool
8
9  (* globals *)
10  val sml_bool_glob     : bool ref
11  val sml_tactic_glob   : tactic ref
12  val sml_string_glob   : string ref
13  val sml_goal_glob     : goal ref
14  val sml_thm_glob      : thm ref
15  val sml_thml_glob     : thm list ref
16
17  (* tests *)
18  val is_thm_value     :
19    (string * PolyML.NameSpace.Values.value) list -> string -> bool
20  val is_local_value   : string -> bool
21  val is_thm           : string -> bool
22  val is_thml          : string -> bool
23  val is_tactic        : string -> bool
24  val is_string        : string -> bool
25  val is_simpset       : string -> bool
26  val is_pointer_eq    : string -> string -> bool
27  val is_stype         : string -> bool
28
29  (* readers *)
30  val thm_of_sml        : string -> (string * thm) option
31  val thml_of_sml       : string list -> thm list option
32  val tactic_of_sml     : real -> string -> tactic
33  val string_of_sml     : string -> string
34  val goal_of_sml       : string -> goal
35
36  (* applying a tactic string *)
37  val app_stac : real -> string -> goal -> goal list option
38
39end
40