Structure Lib
signature Lib =
sig
datatype 'a delta = SAME | DIFF of 'a
datatype frag = datatype HOLPP.frag
datatype ('a, 'b) verdict = PASS of 'a | FAIL of 'b
type 'a cmp = 'a * 'a -> order
type 'a eqf = 'a -> 'a -> bool
type ('a, 'b) istream
type ('a, 'b) subst = {redex: 'a, residue: 'b} list
type 'a set = 'a HOLset.set
val $ : ('a -> 'b) * 'a -> 'b
val ## : ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd
val ?> : ('a, 'c)verdict * ('a -> ('b, 'c)verdict) -> ('b, 'c)verdict
val |-> : ('a * 'b) -> {redex: 'a, residue: 'b}
val |> : 'a * ('a -> 'b) -> 'b
val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
val I : 'a -> 'a
val K : 'a -> 'b -> 'a
val S : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c
val U : ''a list list -> ''a list
val W : ('a -> 'a -> 'b) -> 'a -> 'b
val IN : 'a * 'a set -> bool
val Un : 'a set * 'a set -> 'a set
val Isct : 'a set * 'a set -> 'a set
val -- : 'a set * 'a set -> 'a set
val all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val all : ('a -> bool) -> 'a list -> bool
val apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
val append : 'a list -> 'a list -> 'a list
val appi : (int -> 'a -> unit) -> 'a list -> unit
val apnth : ('a -> 'a) -> int -> 'a list -> 'a list
val apsnd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
val assert : ('a -> bool) -> 'a -> 'a
val assert_exn : ('a -> bool) -> 'a -> exn -> 'a
val assoc1 : ''a -> (''a * 'b) list -> (''a * 'b) option
val assoc2 : ''a -> ('b * ''a) list -> ('b * ''a) option
val assoc : ''a -> (''a * 'b) list -> 'b
val bool_compare : bool cmp
val butlast : 'a list -> 'a list
val can : ('a -> 'b) -> 'a -> bool
val combine : 'a list * 'b list -> ('a * 'b) list
val commafy : string list -> string list
val cons : 'a -> 'a list -> 'a list
val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
val deinitcomment : string -> string
val deinitcommentss : substring -> substring
val delete_trailing_wspace : string -> string
val delta_apply : ('a -> 'a delta) -> 'a -> 'a
val delta_map : ('a -> 'a delta) -> 'a list -> 'a list delta
val delta_pair :
('a -> 'a delta) -> ('b -> 'b delta) -> 'a * 'b -> ('a * 'b) delta
val dict_topsort : ('a, 'a list) Redblackmap.dict -> 'a list
val el : int -> 'a list -> 'a
val end_itlist : ('a -> 'a -> 'a) -> 'a list -> 'a
val end_real_time : Timer.real_timer -> unit
val end_time : Timer.cpu_timer -> unit
val enumerate : int -> 'a list -> (int * 'a) list
val equal : ''a -> ''a -> bool
val exists : ('a -> bool) -> 'a list -> bool
val extract_pc : string -> string * int (* "pc" = "prime count" *)
val filter : ('a -> bool) -> 'a list -> 'a list
val first : ('a -> bool) -> 'a list -> 'a
val first_opt : (int -> 'a -> 'b option) -> 'a list -> 'b option
val flatten : 'a list list -> 'a list
val flip_cmp : 'a cmp -> 'a cmp
val flip_order : order -> order
val foldl_map : ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
val for : int -> int -> (int -> 'a) -> 'a list
val for_se : int -> int -> (int -> unit) -> unit
val front_last : 'a list -> 'a list * 'a
val fst : 'a * 'b -> 'a
val funpow : int -> ('a -> 'a) -> 'a -> 'a
val get_first : ('a -> 'b option) -> 'a list -> 'b option
val hash : int -> string -> int * int -> int
val index : ('a -> bool) -> 'a list -> int
val insert : ''a -> ''a list -> ''a list
val int_sort : int list -> int list
val int_to_string : int -> string
val intersect : ''a list -> ''a list -> ''a list
val inv_img_cmp : ('b -> 'a) -> 'a cmp -> 'b cmp
val is_substring : string -> string -> bool
val itlist2 : ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
val itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val last : 'a list -> 'a
val lex_cmp : ('b cmp * 'c cmp) -> (('a -> 'b) * ('a -> 'c)) -> 'a cmp
val list_compare : 'a cmp -> 'a list cmp
val list_eq : 'a eqf -> 'a list eqf
val list_of_pair : 'a * 'a -> 'a list
val list_of_quadruple : 'a * 'a * 'a * 'a -> 'a list
val list_of_singleton : 'a -> 'a list
val list_of_triple : 'a * 'a * 'a -> 'a list
val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val mapfilter : ('a -> 'b) -> 'a list -> 'b list
val mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
val mapshape : int list -> ('a list -> 'b) list -> 'a list -> 'b list
val measure_cmp : ('a -> int) -> 'a cmp
val mem : ''a -> ''a list -> bool
val mk_istream : ('a -> 'a) -> 'a -> ('a -> 'b) -> ('a, 'b) istream
val mk_set : ''a list -> ''a list
val mlquote : string -> string
val next : ('a, 'b) istream -> ('a, 'b) istream
val null_intersection : ''a list -> ''a list -> bool
val op_U : ('a -> 'a -> bool) -> 'a list list -> 'a list
val op_assoc : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b
val op_assoc1 : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b option
val op_insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
val op_intersect : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
val op_mem : ('a -> 'a -> bool) -> 'a -> 'a list -> bool
val op_mk_set : ('a -> 'a -> bool) -> 'a list -> 'a list
val op_rev_assoc : ('a -> 'a -> bool) -> 'a -> ('b * 'a) list -> 'b
val op_set_diff : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
val op_union : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
val option_compare : 'a cmp -> 'a option cmp
val option_eq : 'a eqf -> 'a option eqf
val pair : 'a -> 'b -> 'a * 'b
val pair_compare : ('a cmp * 'b cmp) -> ('a * 'b) cmp
val pair_eq : 'a eqf -> 'b eqf -> ('a * 'b) eqf
val pair_of_list : 'a list -> 'a * 'a
val partial : exn -> ('a -> 'b option) -> 'a -> 'b
val partition : ('a -> bool) -> 'a list -> 'a list * 'a list
val pluck : ('a -> bool) -> 'a list -> 'a * 'a list
val ppstring : ('a -> HOLPP.pretty) -> 'a -> string
val prime : string -> string
val quadruple : 'a -> 'b -> 'c -> 'd -> 'a * 'b * 'c * 'd
val quadruple_of_list : 'a list -> 'a * 'a * 'a * 'a
val quote : string -> string
val real_time : ('a -> 'b) -> 'a -> 'b
val redres_eq : 'a eqf -> 'b eqf -> {redex:'a,residue:'b} eqf
val repeat : ('a -> 'a) -> 'a -> 'a
val reset : ('a, 'b) istream -> ('a, 'b) istream
val rev_assoc : ''a -> ('b * ''a) list -> 'b
val rev_itlist2 : ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
val rev_itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val rpair : 'a -> 'b -> 'b * 'a
val say : string -> unit
val saying : bool ref
val separate : 'a -> 'a list -> 'a list
val set_diff : ''a list -> ''a list -> ''a list
val set_eq : ''a list -> ''a list -> bool
val single : 'a -> 'a list
val singleton_of_list : 'a list -> 'a
val snd : 'a * 'b -> 'b
val sort : ('a -> 'a -> bool) -> 'a list -> 'a list
val split : ('a * 'b) list -> 'a list * 'b list
val split_after : int -> 'a list -> 'a list * 'a list
val start_real_time : unit -> Timer.real_timer
val start_time : unit -> Timer.cpu_timer
val state : ('a, 'b) istream -> 'b
val str_all : (char -> bool) -> string -> bool
val strcat : string -> string -> string
val string_to_int : string -> int
val subst_assoc : ('a -> bool) -> ('a, 'b)subst -> 'b option
val subst_eq : 'a eqf -> 'b eqf -> ('a,'b) subst eqf
val subtract : ''a list -> ''a list -> ''a list
val swap : 'a * 'b -> 'b * 'a
val time : ('a -> 'b) -> 'a -> 'b
val time_to_string : Time.time -> string
val topsort : ('a -> 'a -> bool) -> 'a list -> 'a list
val total : ('a -> 'b) -> 'a -> 'b option
val triple : 'a -> 'b -> 'c -> 'a * 'b * 'c
val triple_of_list : 'a list -> 'a * 'a * 'a
val try : ('a -> 'b) -> 'a -> 'b
val trye : ('a -> 'b) -> 'a -> 'b
val tryfind : ('a -> 'b) -> 'a list -> 'b
val trypluck': ('a -> 'b option) -> 'a list -> ('b option * 'a list)
val trypluck : ('a -> 'b) -> 'a list -> 'b * 'a list
val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c
val union : ''a list -> ''a list -> ''a list
val unprefix : string -> string -> string
val unprime : string -> string
val unzip : ('a * 'b) list -> 'a list * 'b list
val upto : int -> int -> int list
val vector_topsort : int list vector -> int list
val verdict : ('a -> 'b) -> ('a -> 'c) -> 'a -> ('b, 'c * exn)verdict
val with_exn : ('a -> 'b) -> 'a -> exn -> 'b
val with_flag : 'a ref * 'a -> ('b -> 'c) -> 'b -> 'c
val words2 : string -> string -> string list
val zip : 'a list -> 'b list -> ('a * 'b) list
end
HOL 4, Kananaskis-14