Pure/library/assert_all: new, moved from ZF/ind_syntax.ML

--- a/src/Pure/library.ML	Thu Aug 18 17:41:40 1994 +0200
+++ b/src/Pure/library.ML	Thu Aug 18 17:50:22 1994 +0200
@@ -647,6 +647,12 @@
 fun assert p msg = if p then () else error msg;
 fun deny p msg = if p then error msg else ();
 
+(*Assert pred for every member of l, generating a message if pred fails*)
+fun assert_all pred l msg_fn = 
+  let fun asl [] = ()
+	| asl (x::xs) = if pred x then asl xs
+	                else error (msg_fn x)
+  in  asl l  end;
 
 (* FIXME close file (?) *)
 (*for the "test" target in Makefiles -- signifies successful termination*)