taken over from AFP / Gauss_Jordan

--- a/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:16 2018 +0200
+++ b/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:17 2018 +0200
@@ -40,6 +40,10 @@
 "IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
 by (cases as) (simp add: map_nth)
 
+lemma of_fun_nth:
+"IArray.of_fun f n !! i = f i" if "i < n"
+using that by (simp add: map_nth)
+
 end