src/Pure/library.ML
changeset 8043 0e4434d55df9
parent 7712 c522ec2adc37
child 8418 26eb0c4db5a5
equal deleted inserted replaced
8042:ecdedff41e67 8043:0e4434d55df9
   200   val fold_bal: ('a * 'a -> 'a) -> 'a list -> 'a
   200   val fold_bal: ('a * 'a -> 'a) -> 'a list -> 'a
   201   val access_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> int -> 'a
   201   val access_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> int -> 'a
   202   val accesses_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> 'a list
   202   val accesses_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> 'a list
   203 
   203 
   204   (*orders*)
   204   (*orders*)
   205   datatype order = EQUAL | GREATER | LESS
   205   datatype order = LESS | EQUAL | GREATER
   206   val rev_order: order -> order
   206   val rev_order: order -> order
   207   val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
   207   val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
   208   val int_ord: int * int -> order
   208   val int_ord: int * int -> order
   209   val string_ord: string * string -> order
   209   val string_ord: string * string -> order
   210   val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order
   210   val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order