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