more operations, following Isabelle/ML conventions;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/array.ML	Wed Apr 19 23:27:33 2023 +0200
@@ -0,0 +1,31 @@
+(*  Title:      Pure/General/array.ML
+    Author:     Makarius
+
+Additional operations for structure Array, following Isabelle/ML conventions.
+*)
+
+signature ARRAY =
+sig
+  include ARRAY
+  val nth: 'a array -> int -> 'a
+  val forall: ('a -> bool) -> 'a array -> bool
+  val member: ('a * 'a -> bool) -> 'a array -> 'a -> bool
+  val fold: ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
+  val fold_rev: ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
+end;
+
+structure Array: ARRAY =
+struct
+
+open Array;
+
+fun nth arr i = sub (arr, i);
+
+val forall = all;
+
+fun member eq arr x = exists (fn y => eq (x, y)) arr;
+
+fun fold f arr x = foldl (fn (a, b) => f a b) x arr;
+fun fold_rev f arr x = foldr (fn (a, b) => f a b) x arr;
+
+end;

--- a/src/Pure/ROOT.ML	Wed Apr 19 23:04:26 2023 +0200
+++ b/src/Pure/ROOT.ML	Wed Apr 19 23:27:33 2023 +0200
@@ -21,6 +21,7 @@
 ML_file "General/basics.ML";
 ML_file "General/string.ML";
 ML_file "General/vector.ML";
+ML_file "General/array.ML";
 ML_file "General/symbol_explode.ML";
 
 ML_file "Concurrent/multithreading.ML";