# HG changeset patch
# User haftmann
# Date 1531939877 -7200
# Node ID 90652333fae21244d2f6728661776091ffbbb41c
# Parent  81639cc48d0a7c98d7f874b45087b2b8043ba040
taken over from AFP / Gauss_Jordan

diff -r 81639cc48d0a -r 90652333fae2 src/HOL/Library/IArray.thy
--- 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