# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID d4c06c99a4dca94f489ce3a6ddf0c397ad6b79d2
# Parent  cae4f3d14b0563ba03ce7768c3b4742132a04661
ported IArray to new datatypes

diff -r cae4f3d14b05 -r d4c06c99a4dc src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Library/IArray.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -55,7 +55,7 @@
 | 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]:
@@ -116,4 +116,3 @@
   constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
 
 end
-