1signature backgroundLib =
2sig
3
4  val max : int * int -> int
5  val the : 'a option -> 'a
6  val try_map : ('a -> 'b) -> 'a list -> 'b list
7  val append_lists : 'a list list -> 'a list
8  val diff : ''a list -> ''a list -> ''a list
9  val drop : int -> 'a list -> 'a list
10  val drop_until : ('a -> bool) -> 'a list -> 'a list
11  val every : ('a -> bool) -> 'a list -> bool
12  val lines_from_file : string -> string list
13  val measure_it : string -> ('a -> 'b) -> 'a -> 'b
14  val subset : ''a list -> ''a list -> bool
15  val sum : int list -> int
16  val take : int -> 'a list -> 'a list
17  val take_until : ('a -> bool) -> 'a list -> 'a list
18  val dest_tuple : Term.term -> Term.term list
19  val BINOP1_CONV : Conv.conv -> Conv.conv
20  val REPLACE_CONV : Thm.thm -> Term.term -> Thm.thm
21  val expand_conv : Conv.conv
22  val index_for : ''a -> ''a list -> int
23  val list_dest_pair : Term.term -> Term.term list
24  val list_mk_pair : Term.term list -> Term.term
25  val skip_proofs : bool ref
26  val auto_conv_prove : string -> Term.term -> (Term.term -> Thm.thm) -> Thm.thm
27  val auto_prove :
28     string ->
29     Term.term * ('a list * Term.term -> 'b list * ('c list -> Thm.thm)) ->
30     Thm.thm
31  val clean_name : string -> string
32  val dest_sum_type : Type.hol_type -> Type.hol_type * Type.hol_type
33  val is_inl : Term.term -> bool
34  val is_inr : Term.term -> bool
35  val modify_message : (string -> string) -> exn -> exn
36  val print_error : Term.term -> unit
37  val report_error : string -> exn -> 'a
38
39end
40