equal
deleted
inserted
replaced
49 val plural_s : int -> string |
49 val plural_s : int -> string |
50 val plural_s_for_list : 'a list -> string |
50 val plural_s_for_list : 'a list -> string |
51 val serial_commas : string -> string list -> string list |
51 val serial_commas : string -> string list -> string list |
52 val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list |
52 val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list |
53 val parse_bool_option : bool -> string -> string -> bool option |
53 val parse_bool_option : bool -> string -> string -> bool option |
54 val parse_time_option : string -> string -> Time.time option |
54 val parse_time : string -> string -> Time.time |
55 val string_of_time : Time.time -> string |
55 val string_of_time : Time.time -> string |
56 val nat_subscript : int -> string |
56 val nat_subscript : int -> string |
57 val flip_polarity : polarity -> polarity |
57 val flip_polarity : polarity -> polarity |
58 val prop_T : typ |
58 val prop_T : typ |
59 val bool_T : typ |
59 val bool_T : typ |
69 val is_of_class_const : theory -> string * typ -> bool |
69 val is_of_class_const : theory -> string * typ -> bool |
70 val get_class_def : theory -> string -> (string * term) option |
70 val get_class_def : theory -> string -> (string * term) option |
71 val monomorphic_term : Type.tyenv -> term -> term |
71 val monomorphic_term : Type.tyenv -> term -> term |
72 val specialize_type : theory -> string * typ -> term -> term |
72 val specialize_type : theory -> string * typ -> term -> term |
73 val eta_expand : typ list -> term -> int -> term |
73 val eta_expand : typ list -> term -> int -> term |
74 val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b |
74 val DETERM_TIMEOUT : Time.time -> tactic -> tactic |
75 val DETERM_TIMEOUT : Time.time option -> tactic -> tactic |
|
76 val indent_size : int |
75 val indent_size : int |
77 val pstrs : string -> Pretty.T list |
76 val pstrs : string -> Pretty.T list |
78 val unyxml : string -> string |
77 val unyxml : string -> string |
79 val pretty_maybe_quote : Pretty.T -> Pretty.T |
78 val pretty_maybe_quote : Pretty.T -> Pretty.T |
80 val hash_term : term -> int |
79 val hash_term : term -> int |
236 Pretty.str conj, Pretty.brk 1, p3] |
235 Pretty.str conj, Pretty.brk 1, p3] |
237 | pretty_serial_commas conj (p :: ps) = |
236 | pretty_serial_commas conj (p :: ps) = |
238 p :: Pretty.str "," :: Pretty.brk 1 :: pretty_serial_commas conj ps |
237 p :: Pretty.str "," :: Pretty.brk 1 :: pretty_serial_commas conj ps |
239 |
238 |
240 val parse_bool_option = Sledgehammer_Util.parse_bool_option |
239 val parse_bool_option = Sledgehammer_Util.parse_bool_option |
241 val parse_time_option = Sledgehammer_Util.parse_time_option |
240 val parse_time = Sledgehammer_Util.parse_time |
242 val string_of_time = ATP_Util.string_of_time |
241 val string_of_time = ATP_Util.string_of_time |
243 |
242 |
244 val subscript = implode o map (prefix "\<^sub>") o Symbol.explode |
243 val subscript = implode o map (prefix "\<^sub>") o Symbol.explode |
245 fun nat_subscript n = |
244 fun nat_subscript n = |
246 n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript |
245 n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript |
294 end; |
293 end; |
295 |
294 |
296 val monomorphic_term = ATP_Util.monomorphic_term |
295 val monomorphic_term = ATP_Util.monomorphic_term |
297 val specialize_type = ATP_Util.specialize_type |
296 val specialize_type = ATP_Util.specialize_type |
298 val eta_expand = ATP_Util.eta_expand |
297 val eta_expand = ATP_Util.eta_expand |
299 val time_limit = Sledgehammer_Util.time_limit |
|
300 |
298 |
301 fun DETERM_TIMEOUT delay tac st = |
299 fun DETERM_TIMEOUT delay tac st = |
302 Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ())) |
300 Seq.of_list (the_list (TimeLimit.timeLimit delay (fn () => SINGLE tac st) ())) |
303 |
301 |
304 val indent_size = 2 |
302 val indent_size = 2 |
305 |
303 |
306 val pstrs = Pretty.breaks o map Pretty.str o space_explode " " |
304 val pstrs = Pretty.breaks o map Pretty.str o space_explode " " |
307 |
305 |