diff -r f11bfc151672 -r dae8b7a9a89a src/Pure/General/array.ML
--- /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;