--- a/src/Pure/library.ML Mon Nov 15 22:31:18 2010 +0100
+++ b/src/Pure/library.ML Tue Nov 16 10:33:36 2010 +0100
@@ -97,6 +97,7 @@
val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
+ val forall2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val zip_options: 'a list -> 'b option list -> ('a * 'b) list
val ~~ : 'a list * 'b list -> ('a * 'b) list
val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list
@@ -543,6 +544,10 @@
| fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
| fold2 f _ _ _ = raise UnequalLengths;
+fun forall2 P [] [] = true
+ | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
+ | forall2 P _ _ = false;
+
fun map_split f [] = ([], [])
| map_split f (x :: xs) =
let