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 39 val term_diff : Term.term list -> Term.term list -> Term.term list 40 val term_mem : Term.term -> Term.term list -> bool 41 val term_intersect : Term.term list -> Term.term list -> Term.term list 42 val term_all_distinct : Term.term list -> Term.term list 43 44 val has_failures : bool ref 45 46end 47