changeset 58249 | 180f1b3508ed |
parent 57117 | a2eb1bdb9270 |
child 58266 | d4c06c99a4dc |
--- a/src/HOL/Library/IArray.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/Library/IArray.thy Tue Sep 09 20:51:36 2014 +0200 @@ -13,7 +13,7 @@ lists first. Arrays could be converted back into lists for printing if they were wrapped up in an additional constructor. *} -datatype 'a iarray = IArray "'a list" +datatype_new 'a iarray = IArray "'a list" primrec list_of :: "'a iarray \<Rightarrow> 'a list" where "list_of (IArray xs) = xs"