src/HOL/Library/IArray.thy

 | constant IArray \<rightharpoonup> (SML) "Vector.fromList"
 | constant IArray.all \<rightharpoonup> (SML) "Vector.all"
 | constant IArray.exists \<rightharpoonup> (SML) "Vector.exists"
 
 lemma [code]:
-"size (as :: 'a iarray) = 0"
+"size (as :: 'a iarray) = Suc (length (IArray.list_of as))"
 by (cases as) simp
 
 lemma [code]:
 "size_iarray f as = Suc (size_list f (IArray.list_of as))"
 by (cases as) simp

 
 code_printing
   constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
 
 end
-